Quelle  bug_17155.out  Sprache: unbekannt

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 *) ()