summaryrefslogtreecommitdiff
path: root/test-suite/prerequisite/admit.v
blob: fb3276632da4e43229df0fe0501106e10f9e0783 (plain)
1
2
Axiom proof_admitted : False.
Ltac admit := case proof_admitted.