diff options
| author | coqbot-app[bot] | 2020-11-28 10:04:40 +0000 |
|---|---|---|
| committer | GitHub | 2020-11-28 10:04:40 +0000 |
| commit | 7f1b4176d2606cc965adc09ce5e8346663980240 (patch) | |
| tree | bd840126a6bf77cf5745d216ad2888c45d725113 /tactics | |
| parent | 79946db207944b7bda1287459edfccbbd211ce1e (diff) | |
| parent | 058ac643c5e93da2472e3a0a717b864f49f90b3b (diff) | |
Merge PR #13496: Revert "Remove deprecated tactic cutrewrite."
Reviewed-by: gares
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/equality.ml | 11 | ||||
| -rw-r--r-- | tactics/equality.mli | 4 |
2 files changed, 15 insertions, 0 deletions
diff --git a/tactics/equality.ml b/tactics/equality.ml index 486575d229..fcdd23a9c1 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -1655,6 +1655,17 @@ 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 5a4fe47cab..fdcbbc0e3c 100644 --- a/tactics/equality.mli +++ b/tactics/equality.mli @@ -107,6 +107,10 @@ 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 |