Remove deprecated tactic cutrewrite.

3 files changed, 0 insertions, 6 deletions

diff --git a/doc/tools/docgram/common.edit_mlg b/doc/tools/docgram/common.edit_mlg
index 6625e07d05..9971a03894 100644
--- a/doc/tools/docgram/common.edit_mlg
+++ b/doc/tools/docgram/common.edit_mlg
@@ -1033,9 +1033,6 @@ simple_tactic: [
 | DELETE "unify" constr constr
 | REPLACE "unify" constr constr "with" preident
 | WITH "unify" constr constr OPT ( "with" preident )
-| DELETE "cutrewrite" orient constr
-| REPLACE "cutrewrite" orient constr "in" hyp
-| WITH "cutrewrite" orient constr OPT ( "in" hyp )
 | DELETE "destauto"
 | REPLACE "destauto" "in" hyp
 | WITH "destauto" OPT ( "in" hyp )
diff --git a/doc/tools/docgram/fullGrammar b/doc/tools/docgram/fullGrammar
index 7f4e92fc37..f628c86cf1 100644
--- a/doc/tools/docgram/fullGrammar
+++ b/doc/tools/docgram/fullGrammar
@@ -1535,8 +1535,6 @@ simple_tactic: [
 | "simple" "injection" destruction_arg
 | "dependent" "rewrite" orient constr
 | "dependent" "rewrite" orient constr "in" hyp
-| "cutrewrite" orient constr
-| "cutrewrite" orient constr "in" hyp
 | "decompose" "sum" constr
 | "decompose" "record" constr
 | "absurd" constr
diff --git a/doc/tools/docgram/orderedGrammar b/doc/tools/docgram/orderedGrammar
index 84efc1e36c..3cd5a85654 100644
--- a/doc/tools/docgram/orderedGrammar
+++ b/doc/tools/docgram/orderedGrammar
@@ -1445,7 +1445,6 @@ simple_tactic: [
 | "einjection" OPT destruction_arg OPT ( "as" LIST0 simple_intropattern )
 | "simple" "injection" OPT destruction_arg
 | "dependent" "rewrite" OPT [ "->" | "<-" ] one_term OPT ( "in" ident )
-| "cutrewrite" OPT [ "->" | "<-" ] one_term OPT ( "in" ident )
 | "decompose" "sum" one_term
 | "decompose" "record" one_term
 | "absurd" one_term