blob: 976e60f20c61f1006617ea0086fe9fe551b74908 (
plain)
1
2
3
4
5
6
7
8
9
10
|
Require Import Program.Tactics.
Section visibility.
(* used to anomaly *)
Program Let Fixpoint ev' (n : nat) : bool := _.
Next Obligation. exact true. Qed.
Check ev'.
End visibility.
Fail Check ev'.
|