diff options
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/equality.ml | 20 | ||||
| -rw-r--r-- | tactics/equality.mli | 2 | ||||
| -rw-r--r-- | tactics/tacinterp.ml | 7 |
3 files changed, 20 insertions, 9 deletions
diff --git a/tactics/equality.ml b/tactics/equality.ml index 6770390152..b6c3acface 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -166,11 +166,21 @@ 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) +let general_multi_multi_rewrite with_evars l cl = + let do1 l2r c = general_multi_rewrite l2r with_evars c cl in + let rec doN l2r c = function + | Precisely n when n <= 0 -> tclIDTAC + | Precisely 1 -> do1 l2r c + | Precisely n -> tclTHENFIRST (do1 l2r c) (doN l2r c (Precisely (n-1))) + | RepeatStar -> tclREPEAT_MAIN (do1 l2r c) + | RepeatPlus -> tclTHENFIRST (do1 l2r c) (doN l2r c RepeatStar) + | UpTo n when n<=0 -> tclIDTAC + | UpTo n -> tclTHENFIRST (tclTRY (do1 l2r c)) (doN l2r c (UpTo (n-1))) + in + let rec loop = function + | [] -> tclIDTAC + | (l2r,m,c)::l -> tclTHENFIRST (doN l2r c m) (loop l) + in loop l (* 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 772f9cdc8e..475304fb6c 100644 --- a/tactics/equality.mli +++ b/tactics/equality.mli @@ -49,7 +49,7 @@ 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 + evars_flag -> (bool * multi * 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 effd6f9afb..8de4fcd10b 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -745,7 +745,7 @@ let rec intern_atomic lf ist x = | TacRewrite (ev,l,cl) -> TacRewrite (ev, - List.map (fun (b,c) -> (b,intern_constr_with_bindings ist c)) l, + List.map (fun (b,m,c) -> (b,m,intern_constr_with_bindings ist c)) l, clause_app (intern_hyp_location ist) cl) | TacInversion (inv,hyp) -> TacInversion (intern_inversion_strength lf ist inv, @@ -2107,7 +2107,7 @@ and interp_atomic ist gl = function (* Equality and inversion *) | TacRewrite (ev,l,cl) -> Equality.general_multi_multi_rewrite ev - (List.map (fun (b,c) -> (b, interp_constr_with_bindings ist gl c)) l) + (List.map (fun (b,m,c) -> (b,m,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) @@ -2405,7 +2405,8 @@ let rec subst_atomic subst (t:glob_atomic_tactic_expr) = match t with (* Equality and inversion *) | TacRewrite (ev,l,cl) -> TacRewrite (ev, - List.map (fun (b,c) ->b,subst_raw_with_bindings subst c) l, + List.map (fun (b,m,c) -> + b,m,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) |