From cd8c4fc982c874802546769b1f7df3c2dcfc0579 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Thu, 25 Jul 2019 19:04:12 +0200
Subject: Actually deprecate the `cutrewrite` tactic

The manual was already saying that it was deprecated, but no warning was
emitted.

Fixes #10572
---
 tactics/equality.ml | 9 ++++++++-
 1 file changed, 8 insertions(+), 1 deletion(-)

(limited to 'tactics')

diff --git a/tactics/equality.ml b/tactics/equality.ml
index fc37d5a254..96b61b6994 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -1648,7 +1648,14 @@ let cutSubstClause l2r eqn cls =
     | None ->    cutSubstInConcl l2r eqn
     | Some id -> cutSubstInHyp l2r eqn id
 
-let cutRewriteClause l2r eqn cls = try_rewrite (cutSubstClause l2r eqn cls)
+let warn_deprecated_cutrewrite =
+  CWarnings.create ~name:"deprecated-cutrewrite" ~category:"deprecated"
+    (fun () -> strbrk"\"cutrewrite\" is deprecated. See documentation for proposed replacement.")
+
+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
 
-- 
cgit v1.2.3