Spracherkennung für: .out vermutete Sprache: Unknown {[0] [0] [0]} [Methode: Schwerpunktbildung, einfache Gewichte, sechs Dimensionen]
File "./output/bug5778.v", line 7, characters 7-11:
The command has indeed failed with message:
The term "I" has type "True"
which should be Set, Prop or Type.
In nested Ltac calls to "c", "abs", "abstract b ltac:(())",
"b", "a", "pose (I : I)" and "(I : I)", last term evaluation failed.
[Dauer der Verarbeitung: 0.11 Sekunden, vorverarbeitet 2026-06-04]
