Revert "Remove deprecated tactic cutrewrite."

This reverts commit f3642ad8bdf6d9aa1b411892e5e6815a6a75e4d5.

1 files changed, 11 insertions, 0 deletions

diff --git a/tactics/equality.ml b/tactics/equality.ml
index 486575d229..fcdd23a9c1 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -1655,6 +1655,17 @@ let cutSubstClause l2r eqn cls =
     | None ->    cutSubstInConcl l2r eqn
     | Some id -> cutSubstInHyp l2r eqn id
 
+let warn_deprecated_cutrewrite =
+  CWarnings.create ~name:"deprecated-cutrewrite" ~category:"deprecated"
+    (fun () -> strbrk"\"cutrewrite\" is deprecated. Use \"replace\" instead.")
+
+let cutRewriteClause l2r eqn cls =
+  warn_deprecated_cutrewrite ();
+  try_rewrite (cutSubstClause l2r eqn cls)
+
+let cutRewriteInHyp l2r eqn id = cutRewriteClause l2r eqn (Some id)
+let cutRewriteInConcl l2r eqn = cutRewriteClause l2r eqn None
+
 let substClause l2r c cls =
   Proofview.Goal.enter begin fun gl ->
   let eq = pf_apply get_type_of gl c in