Spracherkennung für: .out vermutete Sprache: Unknown {[0] [0] [0]} [Methode: Schwerpunktbildung, einfache Gewichte, sechs Dimensionen]
File "./output/bug_17155.v", line 6, characters 0-23:
The command has indeed failed with message:
Uncaught Ltac2 exception: Invalid_argument None
File "./output/bug_17155.v", line 8, characters 0-23:
The command has indeed failed with message:
Uncaught Ltac2 exception: Invalid_argument None
Backtrace:
Call M.g
Call bug_17155.M.f (* local *)
Prim <rocq-runtime.plugins.ltac2:throw>
Ltac2 M.g : unit -> 'a
M.g := fun _ => bug_17155.M.f (* local *) ()
[Dauer der Verarbeitung: 0.11 Sekunden, vorverarbeitet 2026-09-29]
