Merge PR #10305: Fix SSR (un)fold of polymorphic terms - issue 9336

Reviewed-by: gares

3 files changed, 47 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
diff --git a/test-suite/ssr/unfold_fold_polyuniv.v b/test-suite/ssr/unfold_fold_polyuniv.v
new file mode 100644
index 0000000000..1a9309bc79
--- /dev/null
+++ b/test-suite/ssr/unfold_fold_polyuniv.v
@@ -0,0 +1,40 @@
+Require Import ssreflect ssrbool.
+
+Set Universe Polymorphism.
+
+Cumulative Variant paths {A} (x:A) : A -> Type
+  := idpath : paths x x.
+
+Register paths as core.eq.type.
+Register idpath as core.eq.refl.
+
+Structure type := Pack {sort; op : rel sort}.
+
+Example unfold_fold (T : type) (x : sort T) (a : op T x x) : op T x x.
+Proof.
+  rewrite /op. rewrite -/(op _ _ _). assumption.
+Qed.
+
+Example pattern_unfold_fold (b:bool) (a := b) : paths a b.
+Proof.
+  rewrite [in X in paths X _]/a.
+  rewrite -[in X in paths X _]/a.
+  constructor.
+Qed.
+
+Example unfold_in_hyp (b:bool) (a := b) : unit.
+Proof.
+  assert (paths a a) as A by reflexivity.
+  rewrite [in X in paths X _]/a in A.
+  rewrite /a in (B := idpath a).
+  rewrite [in X in paths _ X]/a in (C := idpath a).
+  constructor.
+Qed.
+
+Example fold_in_hyp (b:bool) (p := idpath b) : unit.
+Proof.
+  assert (paths (idpath b) (idpath b)) as A by reflexivity.
+  rewrite -[in X in paths X _]/p in A.
+  rewrite -[in X in paths _ X]/p in (C := idpath (idpath b)).
+  constructor.
+Qed.