fixpoint2.v « failure « test-suite - coq - The formal proof system

about summary refs log tree commit diff

path: root/test-suite/failure/fixpoint2.v

blob: 2d2d6a02cd99ceb77fffea5b08b9dc55bfd61b26 (plain)

(* Check Guard in proofs *)

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