diff options
| author | Maxime Dénès | 2019-07-25 19:04:12 +0200 |
|---|---|---|
| committer | Théo Zimmermann | 2019-11-30 12:33:17 +0100 |
| commit | cd8c4fc982c874802546769b1f7df3c2dcfc0579 (patch) | |
| tree | d806c46e2bf9743500886a1854d0da4a480febc5 /tactics/equality.ml | |
| parent | b76db7671bc23238938bc090af0e00b3009f481c (diff) | |
Actually deprecate the `cutrewrite` tactic
The manual was already saying that it was deprecated, but no warning was
emitted.
Fixes #10572
Diffstat (limited to 'tactics/equality.ml')
| -rw-r--r-- | tactics/equality.ml | 9 |
1 files changed, 8 insertions, 1 deletions
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 |