diff options
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/equality.ml | 11 | ||||
| -rw-r--r-- | tactics/equality.mli | 4 | ||||
| -rw-r--r-- | tactics/tacticals.ml | 26 | ||||
| -rw-r--r-- | tactics/tacticals.mli | 4 | ||||
| -rw-r--r-- | tactics/tactics.ml | 7 |
5 files changed, 48 insertions, 4 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 diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml index 24aa178ed2..68afd9a128 100644 --- a/tactics/tacticals.ml +++ b/tactics/tacticals.ml @@ -727,6 +727,32 @@ module New = struct let (loc,_) = evi.Evd.evar_source in Pretype_errors.error_unsolvable_implicit ?loc env sigma evk None + let tclMAPDELAYEDWITHHOLES accept_unresolved_holes l tac = + let rec aux = function + | [] -> tclUNIT () + | x :: l -> + Proofview.Goal.enter begin fun gl -> + let env = Proofview.Goal.env gl in + let sigma_initial = Proofview.Goal.sigma gl in + let (sigma, x) = x env sigma_initial in + Proofview.Unsafe.tclEVARS sigma <*> tac x >>= fun () -> aux l >>= fun () -> + if accept_unresolved_holes then + tclUNIT () + else + tclEVARMAP >>= fun sigma_final -> + try + let () = check_evars env sigma_final sigma sigma_initial in + tclUNIT () + with e when CErrors.noncritical e -> + let e, info = Exninfo.capture e in + tclZERO ~info e + end in + aux l + + (* The following is basically + tclMAPDELAYEDWITHHOLES accept_unresolved_holes [fun _ _ -> (sigma,())] (fun () -> tac) + but with value not necessarily in unit *) + let tclWITHHOLES accept_unresolved_holes tac sigma = tclEVARMAP >>= fun sigma_initial -> if sigma == sigma_initial then tac diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli index e97c5f3c1f..19d08dcc36 100644 --- a/tactics/tacticals.mli +++ b/tactics/tacticals.mli @@ -209,6 +209,10 @@ module New : sig val tclSELECT : Goal_select.t -> 'a tactic -> 'a tactic val tclWITHHOLES : bool -> 'a tactic -> Evd.evar_map -> 'a tactic val tclDELAYEDWITHHOLES : bool -> 'a delayed_open -> ('a -> unit tactic) -> unit tactic + val tclMAPDELAYEDWITHHOLES : bool -> 'a delayed_open list -> ('a -> unit tactic) -> unit tactic + (* in [tclMAPDELAYEDWITHHOLES with_evars l tac] the delayed + argument of [l] are evaluated in the possibly-updated + environment and updated sigma of each new successive goals *) val tclTIMEOUT : int -> unit tactic -> unit tactic val tclTIME : string option -> 'a tactic -> 'a tactic diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 8b38bc1b0a..5aa31092e9 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -2282,10 +2282,9 @@ let left_with_bindings with_evars = constructor_tac with_evars (Some 2) 1 let right_with_bindings with_evars = constructor_tac with_evars (Some 2) 2 let split_with_bindings with_evars l = Tacticals.New.tclMAP (constructor_tac with_evars (Some 1) 1) l -let split_with_delayed_bindings with_evars = - Tacticals.New.tclMAP (fun bl -> - Tacticals.New.tclDELAYEDWITHHOLES with_evars bl - (constructor_tac with_evars (Some 1) 1)) +let split_with_delayed_bindings with_evars bl = + Tacticals.New.tclMAPDELAYEDWITHHOLES with_evars bl + (constructor_tac with_evars (Some 1) 1) let left = left_with_bindings false let simplest_left = left NoBindings |