Adding universe names to polymorphic entry instances.

6 files changed, 29 insertions, 32 deletions

diff --git a/vernac/classes.ml b/vernac/classes.ml
index f4b0015851..3bac4a6555 100644
--- a/vernac/classes.ml
+++ b/vernac/classes.ml
@@ -370,25 +370,24 @@ let context poly l =
       user_err Pp.(str "Anonymous variables not allowed in contexts.")
   in
   let univs =
-    let uctx = Evd.universe_context_set sigma in
     match ctx with
     | [] -> assert false
-    | [_] ->
-      if poly
-      then Polymorphic_const_entry (Univ.ContextSet.to_context uctx)
-      else Monomorphic_const_entry uctx
+    | [_] -> Evd.const_univ_entry ~poly sigma
     | _::_::_ ->
+      (** TODO: explain this little belly dance *)
       if Lib.sections_are_opened ()
       then
         begin
+          let uctx = Evd.universe_context_set sigma in
           Declare.declare_universe_context poly uctx;
-          if poly then Polymorphic_const_entry Univ.UContext.empty
+          if poly then Polymorphic_const_entry ([], Univ.UContext.empty)
           else Monomorphic_const_entry Univ.ContextSet.empty
         end
-      else if poly
-      then Polymorphic_const_entry (Univ.ContextSet.to_context uctx)
+      else if poly then
+        Evd.const_univ_entry ~poly sigma
       else
         begin
+          let uctx = Evd.universe_context_set sigma in
           Declare.declare_universe_context poly uctx;
           Monomorphic_const_entry Univ.ContextSet.empty
         end
diff --git a/vernac/comAssumption.ml b/vernac/comAssumption.ml
index e990f0cd15..8707121306 100644
--- a/vernac/comAssumption.ml
+++ b/vernac/comAssumption.ml
@@ -47,7 +47,7 @@ match local with
 | Discharge when Lib.sections_are_opened () ->
   let ctx = match ctx with
     | Monomorphic_const_entry ctx -> ctx
-    | Polymorphic_const_entry ctx -> Univ.ContextSet.of_context ctx
+    | Polymorphic_const_entry (_, ctx) -> Univ.ContextSet.of_context ctx
   in
   let decl = (Lib.cwd(), SectionLocalAssum ((c,ctx),p,impl), IsAssumption kind) in
   let _ = declare_variable ident decl in
@@ -79,7 +79,7 @@ match local with
   let () = if do_instance then Typeclasses.declare_instance None false gr in
   let () = if is_coe then Class.try_add_new_coercion gr ~local p in
   let inst = match ctx with
-    | Polymorphic_const_entry ctx -> Univ.UContext.instance ctx
+    | Polymorphic_const_entry (_, ctx) -> Univ.UContext.instance ctx
     | Monomorphic_const_entry _ -> Univ.Instance.empty
   in
     (gr,inst,Lib.is_modtype_strict ())
diff --git a/vernac/comInductive.ml b/vernac/comInductive.ml
index 5ff3032ec4..0c39458a57 100644
--- a/vernac/comInductive.ml
+++ b/vernac/comInductive.ml
@@ -450,10 +450,10 @@ let interp_mutual_inductive_gen env0 ~template udecl (uparamsl,paramsl,indl) not
   in
   let univs =
     match uctx with
-    | Polymorphic_const_entry uctx ->
+    | Polymorphic_const_entry (nas, uctx) ->
       if cum then
-        Cumulative_ind_entry (Univ.CumulativityInfo.from_universe_context uctx)
-      else Polymorphic_ind_entry uctx
+        Cumulative_ind_entry (nas, Univ.CumulativityInfo.from_universe_context uctx)
+      else Polymorphic_ind_entry (nas, uctx)
     | Monomorphic_const_entry uctx ->
       Monomorphic_ind_entry uctx
   in
diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml
index 8aa459729c..602314eec3 100644
--- a/vernac/lemmas.ml
+++ b/vernac/lemmas.ml
@@ -228,7 +228,7 @@ let save_remaining_recthms (locality,p,kind) norm univs body opaq i (id,(t_i,(_,
       | Discharge ->
           let impl = false in (* copy values from Vernacentries *)
           let univs = match univs with
-            | Polymorphic_const_entry univs ->
+            | Polymorphic_const_entry (_, univs) ->
               (* What is going on here? *)
               Univ.ContextSet.of_context univs
             | Monomorphic_const_entry univs -> univs
diff --git a/vernac/obligations.ml b/vernac/obligations.ml
index 97ed43c5f4..c2805674e4 100644
--- a/vernac/obligations.ml
+++ b/vernac/obligations.ml
@@ -667,7 +667,7 @@ let declare_obligation prg obl body ty uctx =
       if not opaque then add_hint (Locality.make_section_locality None) prg constant;
       definition_message obl.obl_name;
       let body = match uctx with
-        | Polymorphic_const_entry uctx ->
+        | Polymorphic_const_entry (_, uctx) ->
           Some (DefinedObl (constant, Univ.UContext.instance uctx))
         | Monomorphic_const_entry _ ->
           Some (TermObl (it_mkLambda_or_LetIn_or_clean (mkApp (mkConst constant, args)) ctx))
@@ -1004,10 +1004,7 @@ and solve_obligation_by_tac prg obls i tac =
               solve_by_tac obl.obl_name (evar_of_obligation obl) tac
                 (pi2 prg.prg_kind) (Evd.evar_universe_context evd)
             in
-            let uctx = if pi2 prg.prg_kind
-              then Polymorphic_const_entry (UState.context ctx)
-              else Monomorphic_const_entry (UState.context_set ctx)
-            in
+            let uctx = UState.const_univ_entry ~poly:(pi2 prg.prg_kind) ctx in
             let prg = {prg with prg_ctx = ctx} in
             let def, obl' = declare_obligation prg obl t ty uctx in
               obls.(i) <- obl';
diff --git a/vernac/record.ml b/vernac/record.ml
index 7a4c38e972..5b3fb81d66 100644
--- a/vernac/record.ml
+++ b/vernac/record.ml
@@ -282,7 +282,7 @@ let declare_projections indsp ctx ?(kind=StructureComponent) binder_name coers u
   let (mib,mip) = Global.lookup_inductive indsp in
   let poly = Declareops.inductive_is_polymorphic mib in
   let u = match ctx with
-    | Polymorphic_const_entry ctx -> Univ.UContext.instance ctx
+    | Polymorphic_const_entry (_, ctx) -> Univ.UContext.instance ctx
     | Monomorphic_const_entry ctx -> Univ.Instance.empty
   in
   let paramdecls = Inductive.inductive_paramdecls (mib, u) in
@@ -389,10 +389,10 @@ let declare_structure finite ubinders univs paramimpls params template ?(kind=St
     match univs with
     | Monomorphic_ind_entry ctx ->
       false, Monomorphic_const_entry Univ.ContextSet.empty
-    | Polymorphic_ind_entry ctx ->
-      true, Polymorphic_const_entry ctx
-    | Cumulative_ind_entry cumi ->
-      true, Polymorphic_const_entry (Univ.CumulativityInfo.univ_context cumi)
+    | Polymorphic_ind_entry (nas, ctx) ->
+      true, Polymorphic_const_entry (nas, ctx)
+    | Cumulative_ind_entry (nas, cumi) ->
+      true, Polymorphic_const_entry (nas, Univ.CumulativityInfo.univ_context cumi)
   in
   let binder_name =
     match name with
@@ -480,7 +480,7 @@ let declare_class finite def cum ubinders univs id idbuild paramimpls params ari
 	(DefinitionEntry class_entry, IsDefinition Definition)
       in
       let inst, univs = match univs with
-        | Polymorphic_const_entry uctx -> Univ.UContext.instance uctx, univs
+        | Polymorphic_const_entry (_, uctx) -> Univ.UContext.instance uctx, univs
         | Monomorphic_const_entry _ -> Univ.Instance.empty, Monomorphic_const_entry Univ.ContextSet.empty
       in
       let cstu = (cst, inst) in
@@ -508,11 +508,11 @@ let declare_class finite def cum ubinders univs id idbuild paramimpls params ari
     | _ ->
        let univs =
          match univs with
-         | Polymorphic_const_entry univs ->
+         | Polymorphic_const_entry (nas, univs) ->
            if cum then
-             Cumulative_ind_entry (Univ.CumulativityInfo.from_universe_context univs)
+             Cumulative_ind_entry (nas, Univ.CumulativityInfo.from_universe_context univs)
            else
-             Polymorphic_ind_entry univs
+             Polymorphic_ind_entry (nas, univs)
          | Monomorphic_const_entry univs ->
            Monomorphic_ind_entry univs
        in
@@ -541,7 +541,8 @@ let declare_class finite def cum ubinders univs id idbuild paramimpls params ari
   in
   let univs, ctx_context, fields =
     match univs with
-    | Polymorphic_const_entry univs ->
+    | Polymorphic_const_entry (nas, univs) ->
+      let () = assert (Int.equal (List.length nas) (Univ.UContext.size univs)) in
       let usubst, auctx = Univ.abstract_universes univs in
       let usubst = Univ.make_instance_subst usubst in
       let map c = Vars.subst_univs_level_constr usubst c in
@@ -682,11 +683,11 @@ let definition_structure udecl kind ~template cum poly finite records =
     let data = List.map (fun (arity, implfs, fields) -> (arity, List.map map implfs, fields)) data in
       let univs =
         match univs with
-        | Polymorphic_const_entry univs ->
+        | Polymorphic_const_entry (nas, univs) ->
           if cum then
-            Cumulative_ind_entry (Univ.CumulativityInfo.from_universe_context univs)
+            Cumulative_ind_entry (nas, Univ.CumulativityInfo.from_universe_context univs)
           else
-            Polymorphic_ind_entry univs
+            Polymorphic_ind_entry (nas, univs)
         | Monomorphic_const_entry univs ->
           Monomorphic_ind_entry univs
       in