Quelle  bug_16745.out   Sprache: unbekannt

Rocq < Rocq < 1 goal
  
  ============================
  True

Unnamed_thm < 
Unnamed_thm < Unnamed_thm < Unnamed_thm < Toplevel input, characters 111-112:
>     | match goal with x := ?v |- _ => exact v end].
>                                             ^
Error:
In environment
x := Top.Unnamed_thm_subproof : nat
The term "Top.Unnamed_thm_subproof" has type "nat"
while it is expected to have type "True".

Unnamed_thm <