Library Coq.Compat.AdmitAxiom


Compatibility file for making the admit tactic act similar to Coq v8.4. In 8.4, admit created a new axiom; in 8.5, it just shelves the goal. This compatibility definition is not in the Coq84.v file to avoid loading an inconsistent axiom implicitly.

Axiom proof_admitted : False.
Ltac admit := clear; abstract case proof_admitted.