diff options
| -rw-r--r-- | tactics/equality.ml | 9 | ||||
| -rw-r--r-- | tactics/equality.mli | 8 | ||||
| -rw-r--r-- | tactics/tacinterp.ml | 5 |
3 files changed, 14 insertions, 8 deletions
diff --git a/tactics/equality.ml b/tactics/equality.ml index 62581d74b2..23966b6c29 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -329,11 +329,14 @@ let general_multi_rewrite l2r with_evars ?tac c cl = (general_rewrite_ebindings l2r (occs_of cl.concl_occs) true ?tac c with_evars) do_hyps +type delayed_open_constr_with_bindings = + env -> evar_map -> evar_map * constr with_bindings + let general_multi_multi_rewrite with_evars l cl tac = - let do1 l2r c gl = + let do1 l2r f gl = + let sigma,c = f (pf_env gl) (project gl) in Refiner.tclWITHHOLES with_evars - (general_multi_rewrite l2r with_evars ?tac c.it) - (Evd.merge (project gl) c.sigma) cl gl in + (general_multi_rewrite l2r with_evars ?tac c) sigma cl gl in let rec doN l2r c = function | Precisely n when n <= 0 -> tclIDTAC | Precisely 1 -> do1 l2r c diff --git a/tactics/equality.mli b/tactics/equality.mli index 9986d230bb..b5c147393d 100644 --- a/tactics/equality.mli +++ b/tactics/equality.mli @@ -68,9 +68,13 @@ val general_rewrite_in : val general_multi_rewrite : orientation -> evars_flag -> ?tac:(tactic * conditions) -> constr with_bindings -> clause -> tactic + +type delayed_open_constr_with_bindings = + env -> evar_map -> evar_map * constr with_bindings + val general_multi_multi_rewrite : - evars_flag -> (bool * multi * constr with_bindings sigma) list -> clause -> - (tactic * conditions) option -> tactic + evars_flag -> (bool * multi * delayed_open_constr_with_bindings) list -> + clause -> (tactic * conditions) option -> tactic val replace_in_clause_maybe_by : constr -> constr -> clause -> tactic option -> tactic val replace : constr -> constr -> tactic diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index 719fa7f859..85986503ed 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -2417,9 +2417,8 @@ and interp_atomic ist gl tac = (* Equality and inversion *) | TacRewrite (ev,l,cl,by) -> let l = List.map (fun (b,m,c) -> - let sigma',c = interp_open_constr_with_bindings ist env sigma c in - let _,sigma' = Evarutil.subtract_evars sigma sigma' in - (b,m,{it=c;sigma=sigma'})) l in + let f env sigma = interp_open_constr_with_bindings ist env sigma c in + (b,m,f)) l in let cl = interp_clause ist gl cl in Equality.general_multi_multi_rewrite ev l cl (Option.map (fun by -> tclCOMPLETE (interp_tactic ist by), Equality.Naive) by) |