diff options
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/extratactics.ml4 | 6 | ||||
| -rw-r--r-- | tactics/tactics.ml | 5 | ||||
| -rw-r--r-- | tactics/tactics.mli | 2 |
3 files changed, 1 insertions, 12 deletions
diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4 index 1ffc0519fe..891e2dba51 100644 --- a/tactics/extratactics.ml4 +++ b/tactics/extratactics.ml4 @@ -25,13 +25,9 @@ open Misctypes DECLARE PLUGIN "extratactics" (**********************************************************************) -(* admit, replace, discriminate, injection, simplify_eq *) +(* replace, discriminate, injection, simplify_eq *) (* cutrewrite, dependent rewrite *) -TACTIC EXTEND admit - [ "admit" ] -> [ admit_as_an_axiom ] -END - let replace_in_clause_maybe_by (sigma1,c1) c2 cl tac = Tacticals.New.tclWITHHOLES false (replace_in_clause_maybe_by c1 c2 cl (Option.map Tacinterp.eval_tactic tac)) diff --git a/tactics/tactics.ml b/tactics/tactics.ml index ad6684e25b..b1559da33f 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 diff --git a/tactics/tactics.mli b/tactics/tactics.mli index 6025883fe6..eea4956214 100644 --- a/tactics/tactics.mli +++ b/tactics/tactics.mli @@ -393,8 +393,6 @@ val unify : ?state:Names.transparent_state -> constr -> constr -> unit val tclABSTRACT : Id.t option -> unit Proofview.tactic -> unit Proofview.tactic -val admit_as_an_axiom : unit Proofview.tactic - val abstract_generalize : ?generalize_vars:bool -> ?force_dep:bool -> Id.t -> unit Proofview.tactic val specialize_eqs : Id.t -> tactic |