|
Rocq < foo is defined
Rocq < bar is defined
Rocq < Rocq < Rocq < Rocq < Rocq < Rocq < Rocq < baz is defined
Rocq <
Rocq < 1 goal
============================
True
Unnamed_thm < Top.Unnamed_thm_subproof
Top.Unnamed_thm_subproof
Toplevel input, characters 2-7:
> baz I.
> ^^^^^
Error:
Tactic failure (level 1).
In nested Ltac calls to "baz", "f" (bound to fun f x y => idtac v; f x),
"f" (bound to
fun _ => let v' := v in
constr:((fun _ => ltac:(idtac v'; fail 1)))) and
"(fun _ => ltac:(idtac v'; fail 1))" (with x:=I,
v':=Top.Unnamed_thm_subproof, v:=Top.Unnamed_thm_subproof, H:=H), last term
evaluation failed.
Unnamed_thm <
[ Dauer der Verarbeitung: 0.16 Sekunden
(vorverarbeitet)
]
|
