diff options
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 |