diff options
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/ssr/ssrcommon.ml | 3 | ||||
| -rw-r--r-- | plugins/ssr/ssrequality.ml | 4 |
2 files changed, 7 insertions, 0 deletions
diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml index 56f17703ff..bb53864a93 100644 --- a/plugins/ssr/ssrcommon.ml +++ b/plugins/ssr/ssrcommon.ml @@ -1119,6 +1119,7 @@ let cleartac clr = check_hyps_uniq [] clr; Tactics.clear (hyps_ids clr) (* XXX the k of the redex should percolate out *) let pf_interp_gen_aux gl to_ind ((oclr, occ), t) = let pat = interp_cpattern gl t None in (* UGLY API *) + let gl = pf_merge_uc_of (fst pat) gl in let cl, env, sigma = Tacmach.pf_concl gl, pf_env gl, project gl in let (c, ucst), cl = try fill_occ_pattern ~raise_NoMatch:true env sigma (EConstr.Unsafe.to_constr cl) pat occ 1 @@ -1253,6 +1254,7 @@ let abs_wgen keep_let f gen (gl,args,c) = | _, Some ((x, "@"), Some p) -> let x = hoi_id x in let cp = interp_cpattern gl p None in + let gl = pf_merge_uc_of (fst cp) gl in let (t, ucst), c = try fill_occ_pattern ~raise_NoMatch:true env sigma (EConstr.Unsafe.to_constr c) cp None 1 with NoMatch -> redex_of_pattern env cp, (EConstr.Unsafe.to_constr c) in @@ -1265,6 +1267,7 @@ let abs_wgen keep_let f gen (gl,args,c) = | _, Some ((x, _), Some p) -> let x = hoi_id x in let cp = interp_cpattern gl p None in + let gl = pf_merge_uc_of (fst cp) gl in let (t, ucst), c = try fill_occ_pattern ~raise_NoMatch:true env sigma (EConstr.Unsafe.to_constr c) cp None 1 with NoMatch -> redex_of_pattern env cp, (EConstr.Unsafe.to_constr c) in diff --git a/plugins/ssr/ssrequality.ml b/plugins/ssr/ssrequality.ml index 538d0c4e9a..dbb0f25abf 100644 --- a/plugins/ssr/ssrequality.ml +++ b/plugins/ssr/ssrequality.ml @@ -619,7 +619,11 @@ let rwargtac ?under ?map_redex ist ((dir, mult), (((oclr, occ), grx), (kind, gt) with _ when snd mult = May -> fail := true; (project gl, EConstr.mkProp) in let rwtac gl = let rx = Option.map (interp_rpattern gl) grx in + let gl = match rx with + | None -> gl + | Some (s,_) -> pf_merge_uc_of s gl in let t = interp gt gl in + let gl = pf_merge_uc_of (fst t) gl in (match kind with | RWred sim -> simplintac occ rx sim | RWdef -> if dir = R2L then foldtac occ rx t else unfoldintac occ rx t gt |