diff options
Diffstat (limited to 'tactics/extratactics.ml4')
| -rw-r--r-- | tactics/extratactics.ml4 | 6 |
1 files changed, 1 insertions, 5 deletions
diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4 index 1ffc0519f..891e2dba5 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)) |