blob: f885e31352328e335b7cd68f2f521b6072bf4ade (
plain)
1
2
3
4
5
6
7
8
9
10
|
(* Check that an anomaly is not raised *)
(* It should however eventually succeed... *)
Goal exists x, x.
Proof.
simple refine (ex_intro _ _ _).
shelve.
(* The failure is due to Type(u)<=Prop for u an arbitrary sort
variable being rejected *)
Fail simple refine (_ _).
Abort.
|
