From 058ac643c5e93da2472e3a0a717b864f49f90b3b Mon Sep 17 00:00:00 2001
From: Théo Zimmermann
Date: Fri, 27 Nov 2020 16:22:33 +0100
Subject: Revert "Remove deprecated tactic cutrewrite."

This reverts commit f3642ad8bdf6d9aa1b411892e5e6815a6a75e4d5.
---
 plugins/ltac/extratactics.mlg | 8 +++++++-
 1 file changed, 7 insertions(+), 1 deletion(-)

(limited to 'plugins')

diff --git a/plugins/ltac/extratactics.mlg b/plugins/ltac/extratactics.mlg
index 6ab82b1253..0b5d36b845 100644
--- a/plugins/ltac/extratactics.mlg
+++ b/plugins/ltac/extratactics.mlg
@@ -41,7 +41,7 @@ DECLARE PLUGIN "ltac_plugin"
 
 (**********************************************************************)
 (* replace, discriminate, injection, simplify_eq                      *)
-(* dependent rewrite                                                  *)
+(* cutrewrite, dependent rewrite                                      *)
 
 let with_delayed_uconstr ist c tac =
   let flags = {
@@ -201,6 +201,12 @@ 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