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

Reviewed-by: gares

1 files changed, 40 insertions, 0 deletions

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.