Impressum bug_16462.out   Sprache: unbekannt

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 <