Merge PR #8601: Move bound universe names to abstract contexts

8 files changed, 31 insertions, 41 deletions

diff --git a/vernac/classes.ml b/vernac/classes.ml
index 39919a141a..b0dba2485a 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/comProgramFixpoint.ml b/vernac/comProgramFixpoint.ml
index 3d3d825bd0..d533db7ed9 100644
--- a/vernac/comProgramFixpoint.ml
+++ b/vernac/comProgramFixpoint.ml
@@ -204,7 +204,6 @@ let build_wellfounded (recname,pl,n,bl,arityc,body) poly r measure notation =
         (** FIXME: include locality *)
         let c = Declare.declare_constant recname (DefinitionEntry ce, IsDefinition Definition) in
         let gr = ConstRef c in
-        let () = UnivNames.register_universe_binders gr (Evd.universe_binders sigma) in
         if Impargs.is_implicit_args () || not (List.is_empty impls) then
           Impargs.declare_manual_implicits false gr [impls]
       in
diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml
index 9019fa15d5..150f2c6ee9 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..ac84003266 100644
--- a/vernac/record.ml
+++ b/vernac/record.ml
@@ -277,12 +277,12 @@ let warn_non_primitive_record =
                     strbrk" could not be defined as a primitive record")))
 
 (* We build projections *)
-let declare_projections indsp ctx ?(kind=StructureComponent) binder_name coers ubinders fieldimpls fields =
+let declare_projections indsp ctx ?(kind=StructureComponent) binder_name coers fieldimpls fields =
   let env = Global.env() in
   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
@@ -324,7 +324,6 @@ let declare_projections indsp ctx ?(kind=StructureComponent) binder_name coers u
                 (** Already defined by declare_mind silently *)
                 let kn = Projection.Repr.constant p in
                 Declare.definition_message fid;
-                UnivNames.register_universe_binders (ConstRef kn) ubinders;
                 kn, mkProj (Projection.make p false,mkRel 1)
 	      else
 		let ccl = subst_projection fid subst ti in
@@ -360,7 +359,6 @@ let declare_projections indsp ctx ?(kind=StructureComponent) binder_name coers u
 		      applist (mkConstU (kn,u),proj_args) 
                   in
                   Declare.definition_message fid;
-                  UnivNames.register_universe_binders (ConstRef kn) ubinders;
 		    kn, constr_fip
                 with Type_errors.TypeError (ctx,te) ->
                   raise (NotDefinable (BadTypedProj (fid,ctx,te))) 
@@ -389,10 +387,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
@@ -443,7 +441,7 @@ let declare_structure finite ubinders univs paramimpls params template ?(kind=St
   let map i (_, _, _, fieldimpls, fields, is_coe, coers) =
     let rsp = (kn, i) in (* This is ind path of idstruc *)
     let cstr = (rsp, 1) in
-    let kinds,sp_projs = declare_projections rsp ctx ~kind binder_name.(i) coers ubinders fieldimpls fields in
+    let kinds,sp_projs = declare_projections rsp ctx ~kind binder_name.(i) coers fieldimpls fields in
     let build = ConstructRef cstr in
     let () = if is_coe then Class.try_add_new_coercion build ~local:false poly in
     let () = Recordops.declare_structure(rsp,cstr,List.rev kinds,List.rev sp_projs) in
@@ -480,7 +478,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
@@ -496,9 +494,7 @@ let declare_class finite def cum ubinders univs id idbuild paramimpls params ari
       in
       let cref = ConstRef cst in
       Impargs.declare_manual_implicits false cref [paramimpls];
-      UnivNames.register_universe_binders cref ubinders;
       Impargs.declare_manual_implicits false (ConstRef proj_cst) [List.hd fieldimpls];
-      UnivNames.register_universe_binders (ConstRef proj_cst) ubinders;
       Classes.set_typeclass_transparency (EvalConstRef cst) false false;
       let sub = match List.hd coers with
 	| Some b -> Some ((if b then Backward else Forward), List.hd priorities) 
@@ -508,11 +504,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,8 +537,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 ->
-      let usubst, auctx = Univ.abstract_universes univs in
+    | Polymorphic_const_entry (nas, univs) ->
+      let usubst, auctx = Univ.abstract_universes nas univs in
       let usubst = Univ.make_instance_subst usubst in
       let map c = Vars.subst_univs_level_constr usubst c in
       let fields = Context.Rel.map map fields in
@@ -682,11 +678,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
diff --git a/vernac/record.mli b/vernac/record.mli
index 953d5ec3b6..04984030f7 100644
--- a/vernac/record.mli
+++ b/vernac/record.mli
@@ -20,7 +20,6 @@ val declare_projections :
   ?kind:Decl_kinds.definition_object_kind ->
   Id.t ->
   bool list ->
-  UnivNames.universe_binders ->
   Impargs.manual_implicits list ->
   Constr.rel_context ->
     (Name.t * bool) list * Constant.t option list