diff options
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/equality.ml | 6 | ||||
| -rw-r--r-- | tactics/equality.mli | 2 | ||||
| -rw-r--r-- | tactics/tacinterp.ml | 20 |
3 files changed, 20 insertions, 8 deletions
diff --git a/tactics/equality.ml b/tactics/equality.ml index c5b7aeedfb..4f94ba5953 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -166,6 +166,12 @@ let general_multi_rewrite l2r with_evars c cl = (general_rewrite_ebindings l2r c with_evars) do_hyps +let rec general_multi_multi_rewrite with_evars l cl = match l with + | [] -> tclIDTAC + | (l2r,c)::l -> + tclTHEN (general_multi_rewrite l2r with_evars c cl) + (general_multi_multi_rewrite with_evars l cl) + (* Conditional rewriting, the success of a rewriting is related to the resolution of the conditions by a given tactic *) diff --git a/tactics/equality.mli b/tactics/equality.mli index 36fc995940..772f9cdc8e 100644 --- a/tactics/equality.mli +++ b/tactics/equality.mli @@ -48,6 +48,8 @@ val general_rewrite_in : val general_multi_rewrite : bool -> evars_flag -> constr with_ebindings -> clause -> tactic +val general_multi_multi_rewrite : + evars_flag -> (bool * constr with_ebindings) list -> clause -> tactic val conditional_rewrite : bool -> tactic -> constr with_ebindings -> tactic val conditional_rewrite_in : diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index 944b7710a5..dc4b3822f7 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -744,9 +744,11 @@ let rec intern_atomic lf ist x = | TacTransitivity c -> TacTransitivity (intern_constr ist c) (* Equality and inversion *) - | TacRewrite (b,ev,c,cl) -> - TacRewrite (b,ev,intern_constr_with_bindings ist c, - clause_app (intern_hyp_location ist) cl) + | TacRewrite (ev,l,cl) -> + TacRewrite + (ev, + List.map (fun (b,c) -> (b,intern_constr_with_bindings ist c)) l, + clause_app (intern_hyp_location ist) cl) | TacInversion (inv,hyp) -> TacInversion (intern_inversion_strength lf ist inv, intern_quantified_hypothesis ist hyp) @@ -2158,9 +2160,9 @@ and interp_atomic ist gl = function | TacTransitivity c -> h_transitivity (pf_interp_constr ist gl c) (* Equality and inversion *) - | TacRewrite (b,ev,c,cl) -> - Equality.general_multi_rewrite b ev - (interp_constr_with_bindings ist gl c) + | TacRewrite (ev,l,cl) -> + Equality.general_multi_multi_rewrite ev + (List.map (fun (b,c) -> (b, interp_constr_with_bindings ist gl c)) l) (interp_clause ist gl cl) | TacInversion (DepInversion (k,c,ids),hyp) -> Inv.dinv k (option_map (pf_interp_constr ist gl) c) @@ -2451,8 +2453,10 @@ let rec subst_atomic subst (t:glob_atomic_tactic_expr) = match t with | TacTransitivity c -> TacTransitivity (subst_rawconstr subst c) (* Equality and inversion *) - | TacRewrite (b,ev,c,cl) -> - TacRewrite (b,ev,subst_raw_with_bindings subst c,cl) + | TacRewrite (ev,l,cl) -> + TacRewrite (ev, + List.map (fun (b,c) ->b,subst_raw_with_bindings subst c) l, + cl) | TacInversion (DepInversion (k,c,l),hyp) -> TacInversion (DepInversion (k,option_map (subst_rawconstr subst) c,l),hyp) | TacInversion (NonDepInversion _,_) as x -> x |