diff options
| author | Théo Zimmermann | 2019-12-02 07:42:31 +0100 |
|---|---|---|
| committer | Théo Zimmermann | 2019-12-02 07:42:31 +0100 |
| commit | 31e109671896ef42653b1fcf239d8ebe1424c3da (patch) | |
| tree | 8ce9d6865ca970e5675fb90b452edb735cdf8b14 /tactics | |
| parent | 73f329333c6123a512ca975da949bec3778ce151 (diff) | |
| parent | a394876327dbe8af8410e8e91c01a363fd2d4cdf (diff) | |
Merge PR #10575: Clean up deprecations
Reviewed-by: Zimmi48
Reviewed-by: silene
Diffstat (limited to 'tactics')
| -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 |