summaryrefslogtreecommitdiff
path: root/test-suite/failure/fixpoint2.v
blob: 7f11a99b165a9424ca9f72db6ebe99f9519c53d1 (plain)
1
2
3
4
5
6
(* Check Guard in proofs *)

Goal nat->nat.
fix f 1.
intro n; apply f; assumption.
Fail Guarded.