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.

3 files changed, 75 insertions, 18 deletions

diff --git a/test-suite/output/UnivBinders.out b/test-suite/output/UnivBinders.out
index 904ff68aa..1bacb7513 100644
--- a/test-suite/output/UnivBinders.out
+++ b/test-suite/output/UnivBinders.out
@@ -1,12 +1,55 @@
+NonCumulative Inductive Empty@{u} : Type@{u} :=  
+NonCumulative Record PWrap (A : Type@{u}) : Type@{u} := pwrap { punwrap : A }
+
+PWrap has primitive projections with eta conversion.
+For PWrap: Argument scope is [type_scope]
+For pwrap: Argument scopes are [type_scope _]
+punwrap@{u} = 
+fun (A : Type@{u}) (p : PWrap@{u} A) => punwrap _ p
+     : forall A : Type@{u}, PWrap@{u} A -> A
+(* u |=  *)
+
+punwrap is universe polymorphic
+Argument scopes are [type_scope _]
+NonCumulative Record RWrap (A : Type@{u}) : Type@{u} := rwrap { runwrap : A }
+
+For RWrap: Argument scope is [type_scope]
+For rwrap: Argument scopes are [type_scope _]
+runwrap@{u} = 
+fun (A : Type@{u}) (r : RWrap@{u} A) => let (runwrap) := r in runwrap
+     : forall A : Type@{u}, RWrap@{u} A -> A
+(* u |=  *)
+
+runwrap is universe polymorphic
+Argument scopes are [type_scope _]
+Wrap@{u} = fun A : Type@{u} => A
+     : Type@{u} -> Type@{u}
+(* u |=  *)
+
+Wrap is universe polymorphic
+Argument scope is [type_scope]
+wrap@{u} = 
+fun (A : Type@{u}) (Wrap : Wrap@{u} A) => Wrap
+     : forall A : Type@{u}, Wrap@{u} A -> A
+(* u |=  *)
+
+wrap is universe polymorphic
+Arguments A, Wrap are implicit and maximally inserted
+Argument scopes are [type_scope _]
 bar@{u} = nat
      : Wrap@{u} Set
 (* u |= Set < u
          *)
 
 bar is universe polymorphic
-foo@{u Top.8 v} = 
-Type@{Top.8} -> Type@{v} -> Type@{u}
-     : Type@{max(u+1, Top.8+1, v+1)}
-(* u Top.8 v |=  *)
+foo@{u Top.17 v} = 
+Type@{Top.17} -> Type@{v} -> Type@{u}
+     : Type@{max(u+1, Top.17+1, v+1)}
+(* u Top.17 v |=  *)
 
 foo is universe polymorphic
+Monomorphic mono = Type@{u}
+     : Type@{u+1}
+(* u |=  *)
+
+mono is not universe polymorphic
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.
diff --git a/vernac/record.ml b/vernac/record.ml
index e465e0616..0819dadb4 100644
--- a/vernac/record.ml
+++ b/vernac/record.ml
@@ -266,11 +266,10 @@ let warn_non_primitive_record =
                     strbrk" could not be defined as a primitive record")))
 
 (* We build projections *)
-let declare_projections indsp ?(kind=StructureComponent) binder_name coers ubinders fieldimpls fields =
+let declare_projections indsp ctx ?(kind=StructureComponent) binder_name coers ubinders fieldimpls fields =
   let env = Global.env() in
   let (mib,mip) = Global.lookup_inductive indsp in
   let poly = Declareops.inductive_is_polymorphic mib in
-  let ctx = Univ.AUContext.repr (Declareops.inductive_polymorphic_context mib) in
   let u = Univ.UContext.instance ctx in
   let paramdecls = Inductive.inductive_paramdecls (mib, u) in
   let indu = indsp, u in
@@ -394,7 +393,7 @@ let declare_structure finite ubinders univs id idbuild paramimpls params arity t
   let type_constructor = it_mkProd_or_LetIn ind fields in
   let poly, ctx =
     match univs with
-    | Monomorphic_ind_entry ctx -> false, ctx
+    | Monomorphic_ind_entry ctx -> false, Univ.UContext.empty
     | Polymorphic_ind_entry ctx -> true, ctx
     | Cumulative_ind_entry cumi -> true, (Univ.CumulativityInfo.univ_context cumi)
   in
@@ -430,20 +429,13 @@ let declare_structure finite ubinders univs id idbuild paramimpls params arity t
     else
        mie
   in
-  let kn = Command.declare_mutual_inductive_with_eliminations mie Universes.empty_binders [(paramimpls,[])] in
+  let kn = Command.declare_mutual_inductive_with_eliminations mie ubinders [(paramimpls,[])] in
   let rsp = (kn,0) in (* This is ind path of idstruc *)
   let cstr = (rsp,1) in
-  let fields =
-    if poly then
-      let subst, _ = Univ.abstract_universes ctx in
-      Context.Rel.map (fun c -> Vars.subst_univs_level_constr subst c) fields
-    else fields
-  in
-  let kinds,sp_projs = declare_projections rsp ~kind binder_name coers ubinders fieldimpls fields in
+  let kinds,sp_projs = declare_projections rsp ctx ~kind binder_name coers ubinders fieldimpls fields in
   let build = ConstructRef cstr in
   let () = if is_coe then Class.try_add_new_coercion build ~local:false poly in
   Recordops.declare_structure(rsp,cstr,List.rev kinds,List.rev sp_projs);
-  Universes.register_universe_binders (IndRef rsp) ubinders;
   rsp
 
 let implicits_of_context ctx =