diff options
Diffstat (limited to 'tactics/tactics.ml')
| -rw-r--r-- | tactics/tactics.ml | 5 |
1 files changed, 0 insertions, 5 deletions
diff --git a/tactics/tactics.ml b/tactics/tactics.ml index ad6684e25..b1559da33 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -4411,11 +4411,6 @@ let tclABSTRACT name_op tac = in abstract_subproof s gk tac -let admit_as_an_axiom = - Proofview.tclUNIT () >>= fun () -> (* delay for Coqlib.build_coq_proof_admitted *) - simplest_case (Coqlib.build_coq_proof_admitted ()) <*> - Proofview.mark_as_unsafe - let unify ?(state=full_transparent_state) x y = Proofview.Goal.nf_enter begin fun gl -> try |