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

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