diff options
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/eqdecide.ml | 4 | ||||
| -rw-r--r-- | tactics/equality.ml | 11 | ||||
| -rw-r--r-- | tactics/equality.mli | 4 |
3 files changed, 17 insertions, 2 deletions
diff --git a/tactics/eqdecide.ml b/tactics/eqdecide.ml index d4cc193eb3..9b3f9053cd 100644 --- a/tactics/eqdecide.ml +++ b/tactics/eqdecide.ml @@ -123,8 +123,8 @@ let idy = Id.of_string "y" let mkGenDecideEqGoal rectype ops g = let hypnames = pf_ids_set_of_hyps g in - let xname = next_ident_away idx hypnames - and yname = next_ident_away idy hypnames in + let xname = next_ident_away idx hypnames in + let yname = next_ident_away idy (Id.Set.add xname hypnames) in (mkNamedProd (make_annot xname Sorts.Relevant) rectype (mkNamedProd (make_annot yname Sorts.Relevant) rectype (mkDecideEqGoal true ops 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 |