[vernac] Improve alpha-renaming in record projection types

2 files changed, 54 insertions, 0 deletions

diff --git a/test-suite/output/RecordProjParameter.out b/test-suite/output/RecordProjParameter.out
new file mode 100644
index 0000000000..91ae4b6511
--- /dev/null
+++ b/test-suite/output/RecordProjParameter.out
@@ -0,0 +1,33 @@
+t1 : Atype -> forall a : Type, a
+
+t1 is not universe polymorphic
+Arguments t1 _ _%type_scope
+t1 is transparent
+Expands to: Constant RecordProjParameter.t1
+t3 : forall a0 : Atype, t2 a0
+
+t3 is not universe polymorphic
+t3 is transparent
+Expands to: Constant RecordProjParameter.t3
+u1 : Btype -> forall b b0 : Type, b * b0
+
+u1 is not universe polymorphic
+Arguments u1 _ (_ _)%type_scope
+u1 is transparent
+Expands to: Constant RecordProjParameter.u1
+u3 : forall b1 : Btype, u2 b1
+
+u3 is not universe polymorphic
+u3 is transparent
+Expands to: Constant RecordProjParameter.u3
+v1 : Ctype -> forall c0 : Type, c0
+
+v1 is not universe polymorphic
+Arguments v1 _ _%type_scope
+v1 is transparent
+Expands to: Constant RecordProjParameter.v1
+v3 : forall c : Ctype, v2 c
+
+v3 is not universe polymorphic
+v3 is transparent
+Expands to: Constant RecordProjParameter.v3
diff --git a/test-suite/output/RecordProjParameter.v b/test-suite/output/RecordProjParameter.v
new file mode 100644
index 0000000000..8b892c694c
--- /dev/null
+++ b/test-suite/output/RecordProjParameter.v
@@ -0,0 +1,21 @@
+Record Atype : Type :=
+  { t1 : forall (a : Type), a
+  ; t2 : Type
+  ; t3 : t2 }.
+About t1.
+About t3.
+
+Record Btype : Type :=
+  { u1 : forall (b : Type) (b0 : Type), b * b0
+  ; u2 : Type
+  ; u3 : u2 }.
+About u1.
+About u3.
+
+Record Ctype : Type :=
+  { v1 : forall (c0 : Type), c0
+  ; v2 : Type
+  ; v3 : v2
+  }.
+About v1.
+About v3.