Fix defining non primitive projections with abstracted universes.

I think this only affects printing (in the new test you would get
[Var (0)] when printing runwrap) but is still ugly.

1 files changed, 24 insertions, 2 deletions

diff --git a/test-suite/output/UnivBinders.v b/test-suite/output/UnivBinders.v
index 8656ff1a3..2c378e795 100644
--- a/test-suite/output/UnivBinders.v
+++ b/test-suite/output/UnivBinders.v
@@ -2,12 +2,34 @@ Set Universe Polymorphism.
 Set Printing Universes.
 Unset Strict Universe Declaration.
 
-Class Wrap A := wrap : A.
+(* universe binders on inductive types and record projections *)
+Inductive Empty@{u} : Type@{u} := .
+Print Empty.
 
-Instance bar@{u} : Wrap@{u} Set. Proof nat.
+Set Primitive Projections.
+Record PWrap@{u} (A:Type@{u}) := pwrap { punwrap : A }.
+Print PWrap.
+Print punwrap.
+
+Unset Primitive Projections.
+Record RWrap@{u} (A:Type@{u}) := rwrap { runwrap : A }.
+Print RWrap.
+Print runwrap.
+
+(* universe binders also go on the constants for operational typeclasses. *)
+Class Wrap@{u} (A:Type@{u}) := wrap : A.
+Print Wrap.
+Print wrap.
+
+(* Instance in lemma mode used to ignore the binders. *)
+Instance bar@{u} : Wrap@{u} Set. Proof. exact nat. Qed.
 Print bar.
 
 (* The universes in the binder come first, then the extra universes in
    order of appearance. *)
 Definition foo@{u +} := Type -> Type@{v} -> Type@{u}.
 Print foo.
+
+(* Binders even work with monomorphic definitions! *)
+Monomorphic Definition mono@{u} := Type@{u}.
+Print mono.