From f3642ad8bdf6d9aa1b411892e5e6815a6a75e4d5 Mon Sep 17 00:00:00 2001
From: Théo Zimmermann
Date: Tue, 8 Sep 2020 16:51:05 +0200
Subject: Remove deprecated tactic cutrewrite.

---
 plugins/ltac/extratactics.mlg | 8 +-------
 1 file changed, 1 insertion(+), 7 deletions(-)

(limited to 'plugins')

diff --git a/plugins/ltac/extratactics.mlg b/plugins/ltac/extratactics.mlg
index 66c72a30a2..4f20e5a800 100644
--- a/plugins/ltac/extratactics.mlg
+++ b/plugins/ltac/extratactics.mlg
@@ -43,7 +43,7 @@ DECLARE PLUGIN "ltac_plugin"
 
 (**********************************************************************)
 (* replace, discriminate, injection, simplify_eq                      *)
-(* cutrewrite, dependent rewrite                                      *)
+(* dependent rewrite                                                  *)
 
 let with_delayed_uconstr ist c tac =
   let flags = {
@@ -203,12 +203,6 @@ TACTIC EXTEND dependent_rewrite
     -> { rewriteInHyp b c id }
 END
 
-TACTIC EXTEND cut_rewrite
-| [ "cutrewrite" orient(b) constr(eqn) ] -> { cutRewriteInConcl b eqn }
-| [ "cutrewrite" orient(b) constr(eqn) "in" hyp(id) ]
-    -> { cutRewriteInHyp b eqn id }
-END
-
 (**********************************************************************)
 (* Decompose                                                          *)
 
-- 
cgit v1.2.3