diff options
| author | Clément Pit-Claudel | 2020-09-08 14:52:36 -0400 |
|---|---|---|
| committer | Clément Pit-Claudel | 2020-09-08 14:52:36 -0400 |
| commit | 0ab3e7f16064be178e7c48aeef5252cc0d0d3109 (patch) | |
| tree | 56d503cc9c227adc903653661d517f58c420ba17 /tactics | |
| parent | d19175c1c7e64777129742dbc986521efa61072e (diff) | |
| parent | f3642ad8bdf6d9aa1b411892e5e6815a6a75e4d5 (diff) | |
Merge PR #12993: Remove deprecated tactic cutrewrite.
Reviewed-by: cpitclaudel
Reviewed-by: ppedrot
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/equality.ml | 11 | ||||
| -rw-r--r-- | tactics/equality.mli | 4 |
2 files changed, 0 insertions, 15 deletions
diff --git a/tactics/equality.ml b/tactics/equality.ml index 26ae35a79d..8478c1957a 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -1651,17 +1651,6 @@ 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 diff --git a/tactics/equality.mli b/tactics/equality.mli index fdcbbc0e3c..5a4fe47cab 100644 --- a/tactics/equality.mli +++ b/tactics/equality.mli @@ -107,10 +107,6 @@ val dEqThen : keep_proofs:(bool option) -> evars_flag -> (clear_flag -> constr - val make_iterated_tuple : env -> evar_map -> constr -> (constr * types) -> evar_map * (constr * constr * constr) -(* The family cutRewriteIn expect an equality statement *) -val cutRewriteInHyp : bool -> types -> Id.t -> unit Proofview.tactic -val cutRewriteInConcl : bool -> constr -> unit Proofview.tactic - (* The family rewriteIn expect the proof of an equality *) val rewriteInHyp : bool -> constr -> Id.t -> unit Proofview.tactic val rewriteInConcl : bool -> constr -> unit Proofview.tactic |