test-suite/success/pose.v


1
2
3
4
5
6
7
8
9

(* Test syntax *)

Goal 0=0.
pose proof (a := I).
Fail clearbody a.
epose proof (b := fun _ => eq_refl).
Fail clearbody b.
exact (b a).
Qed.