Using UInfoInd for universes in inductive types

It stores both universe constraints and subtyping information for
blocks of inductive declarations.

At this stage the there is no inference or checking implemented. The
subtyping information simply encodes equality of levels for the condition of
subtyping.

22 files changed, 60 insertions, 64 deletions

diff --git a/API/API.mli b/API/API.mli
index e2c43dab8..cea879ba3 100644
--- a/API/API.mli
+++ b/API/API.mli
@@ -86,6 +86,8 @@ sig
   type universe_context = UContext.t
   [@@ocaml.deprecated "alias of API.Names.UContext.t"]
 
+  type universe_info_ind = Univ.UInfoInd.t
+
   module LSet : module type of struct include Univ.LSet end
   module ContextSet : 
   sig
@@ -1093,8 +1095,7 @@ sig
         mind_nparams_rec : int;
         mind_params_ctxt : Context.Rel.t;
         mind_polymorphic : bool;
-        mind_universes : Univ.UContext.t;
-        mind_subtyping : Univ.universe_context;
+        mind_universes : Univ.universe_info_ind;
         mind_private : bool option;
         mind_typing_flags : Declarations.typing_flags;
       }
diff --git a/engine/universes.ml b/engine/universes.ml
index 955e1d8b5..ad53bf898 100644
--- a/engine/universes.ml
+++ b/engine/universes.ml
@@ -338,14 +338,14 @@ let fresh_constant_instance env c inst =
 let fresh_inductive_instance env ind inst = 
   let mib, mip = Inductive.lookup_mind_specif env ind in
     if mib.Declarations.mind_polymorphic then
-      let inst, ctx = fresh_instance_from mib.Declarations.mind_universes inst in
+      let inst, ctx = fresh_instance_from (Univ.UInfoInd.univ_context mib.Declarations.mind_universes) inst in
 	((ind,inst), ctx)
     else ((ind,Instance.empty), ContextSet.empty)
 
 let fresh_constructor_instance env (ind,i) inst = 
   let mib, mip = Inductive.lookup_mind_specif env ind in
     if mib.Declarations.mind_polymorphic then
-      let inst, ctx = fresh_instance_from mib.Declarations.mind_universes inst in
+      let inst, ctx = fresh_instance_from (Univ.UInfoInd.univ_context mib.Declarations.mind_universes) inst in
 	(((ind,i),inst), ctx)
     else (((ind,i),Instance.empty), ContextSet.empty)
 
@@ -360,14 +360,14 @@ let unsafe_constant_instance env c =
 let unsafe_inductive_instance env ind = 
   let mib, mip = Inductive.lookup_mind_specif env ind in
     if mib.Declarations.mind_polymorphic then
-      let inst, ctx = unsafe_instance_from mib.Declarations.mind_universes in
+      let inst, ctx = unsafe_instance_from (Univ.UInfoInd.univ_context mib.Declarations.mind_universes) in
 	((ind,inst), ctx)
     else ((ind,Instance.empty), UContext.empty)
 
 let unsafe_constructor_instance env (ind,i) = 
   let mib, mip = Inductive.lookup_mind_specif env ind in
     if mib.Declarations.mind_polymorphic then
-      let inst, ctx = unsafe_instance_from mib.Declarations.mind_universes in
+      let inst, ctx = unsafe_instance_from (Univ.UInfoInd.univ_context mib.Declarations.mind_universes) in
 	(((ind,i),inst), ctx)
     else (((ind,i),Instance.empty), UContext.empty)
 
@@ -460,7 +460,7 @@ let type_of_reference env r =
   | IndRef ind ->
      let (mib, oib as specif) = Inductive.lookup_mind_specif env ind in
        if mib.mind_polymorphic then
-	 let inst, ctx = fresh_instance_from mib.mind_universes None in
+	 let inst, ctx = fresh_instance_from (Univ.UInfoInd.univ_context mib.mind_universes) None in
 	 let ty = Inductive.type_of_inductive env (specif, inst) in
 	   ty, ctx
        else
@@ -469,7 +469,7 @@ let type_of_reference env r =
   | ConstructRef cstr ->
      let (mib,oib as specif) = Inductive.lookup_mind_specif env (inductive_of_constructor cstr) in
        if mib.mind_polymorphic then
-	 let inst, ctx = fresh_instance_from mib.mind_universes None in
+	 let inst, ctx = fresh_instance_from (Univ.UInfoInd.univ_context mib.mind_universes) None in
 	   Inductive.type_of_constructor (cstr,inst) specif, ctx
        else Inductive.type_of_constructor (cstr,Instance.empty) specif, ContextSet.empty
 
diff --git a/kernel/declarations.ml b/kernel/declarations.ml
index 9536407d3..1bb1e885f 100644
--- a/kernel/declarations.ml
+++ b/kernel/declarations.ml
@@ -188,9 +188,7 @@ type mutual_inductive_body = {
 
     mind_polymorphic : bool; (** Is it polymorphic or not *)
 
-    mind_universes : Univ.universe_context; (** Local universe variables and constraints *)
-
-    mind_subtyping : Univ.universe_context; (** Constraints for subtyping *)
+    mind_universes : Univ.universe_info_ind; (** Local universe variables and constraints together with subtyping constraints *)
 
     mind_private : bool option; (** allow pattern-matching: Some true ok, Some false blocked *)
 
diff --git a/kernel/declareops.ml b/kernel/declareops.ml
index 47a23c855..cdea468ad 100644
--- a/kernel/declareops.ml
+++ b/kernel/declareops.ml
@@ -261,19 +261,18 @@ let subst_mind_body sub mib =
     mind_packets = Array.smartmap (subst_mind_packet sub) mib.mind_packets ;
     mind_polymorphic = mib.mind_polymorphic;
     mind_universes = mib.mind_universes;
-    mind_subtyping = mib.mind_subtyping;
     mind_private = mib.mind_private;
     mind_typing_flags = mib.mind_typing_flags;
   }
 
 let inductive_instance mib =
   if mib.mind_polymorphic then
-    Univ.UContext.instance mib.mind_universes
+    Univ.UContext.instance (Univ.UInfoInd.univ_context mib.mind_universes)
   else Univ.Instance.empty
 
 let inductive_context mib =
   if mib.mind_polymorphic then 
-    Univ.instantiate_univ_context mib.mind_universes 
+    Univ.instantiate_univ_context (Univ.UInfoInd.univ_context mib.mind_universes)
   else Univ.UContext.empty
 
 (** {6 Hash-consing of inductive declarations } *)
@@ -306,7 +305,7 @@ let hcons_mind mib =
   { mib with
     mind_packets = Array.smartmap hcons_mind_packet mib.mind_packets;
     mind_params_ctxt = hcons_rel_context mib.mind_params_ctxt;
-    mind_universes = Univ.hcons_universe_context mib.mind_universes }
+    mind_universes = Univ.hcons_universe_info_ind mib.mind_universes }
 
 (** {6 Stm machinery } *)
 
diff --git a/kernel/entries.mli b/kernel/entries.mli
index 88584e3b3..97c28025a 100644
--- a/kernel/entries.mli
+++ b/kernel/entries.mli
@@ -50,7 +50,7 @@ type mutual_inductive_entry = {
   mind_entry_params : (Id.t * local_entry) list;
   mind_entry_inds : one_inductive_entry list;
   mind_entry_polymorphic : bool; 
-  mind_entry_universes : Univ.universe_context * Univ.universe_context;
+  mind_entry_universes : Univ.universe_info_ind;
   (* universe constraints and the constraints for subtyping of
      inductive types in the block. *)
   mind_entry_private : bool option;
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index 5d928facc..94bf1a770 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -220,7 +220,7 @@ let typecheck_inductive env mie =
   (* Check unicity of names *)
   mind_check_names mie;
   (* Params are typed-checked here *)
-  let env' = push_context (fst mie.mind_entry_universes) env in
+  let env' = push_context (Univ.UInfoInd.univ_context mie.mind_entry_universes) env in
   let (env_params,paramsctxt) = infer_local_decls env' mie.mind_entry_params in
   (* We first type arity of each inductive definition *)
   (* This allows building the environment of arities and to share *)
@@ -822,10 +822,10 @@ let build_inductive env p prv ctx env_ar paramsctxt kn isrecord isfinite inds nm
   let hyps = used_section_variables env inds in
   let nparamargs = Context.Rel.nhyps paramsctxt in
   let nparamsctxt = Context.Rel.length paramsctxt in
-  let substunivs, ctxunivs = Univ.abstract_universes p (fst ctx) in
-  let substsbt, ctxsbt = Univ.abstract_universes p (snd ctx) in
+  let substunivs, ctxunivs = Univ.abstract_universes p (Univ.UInfoInd.univ_context ctx) in
+  let substsubtyp, ctxsubtyp = Univ.abstract_universes p (Univ.UInfoInd.subtyp_context ctx) in
   let paramsctxt = Vars.subst_univs_level_context substunivs paramsctxt in
-  let env_ar = 
+  let env_ar =
     let ctxunivs = Environ.rel_context env_ar in 
     let ctxunivs' = Vars.subst_univs_level_context substunivs ctxunivs in
       Environ.push_rel_context ctxunivs' env
@@ -842,9 +842,6 @@ let build_inductive env p prv ctx env_ar paramsctxt kn isrecord isfinite inds nm
     let consnrealargs =
       Array.map (fun (d,_) -> Context.Rel.nhyps d - nparamargs)
 	splayed_lc in
-    (* Check that the subtyping constraints (inferred outside kernel)
-       are valid. If so return (), otherwise raise an anomaly! *)
-    let () = () in
     (* Elimination sorts *)
     let arkind,kelim = 
       match ar_kind with
@@ -924,8 +921,7 @@ let build_inductive env p prv ctx env_ar paramsctxt kn isrecord isfinite inds nm
       mind_params_ctxt = paramsctxt;
       mind_packets = packets;
       mind_polymorphic = p;
-      mind_universes = ctxunivs;
-      mind_subtyping = ctxsbt;
+      mind_universes = Univ.UInfoInd.make (ctxunivs, ctxsubtyp);
       mind_private = prv;
       mind_typing_flags = Environ.typing_flags env;
     }
diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index f3b03252d..0f0dc0d60 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -55,7 +55,7 @@ let inductive_paramdecls (mib,u) =
 
 let instantiate_inductive_constraints mib u =
   if mib.mind_polymorphic then
-    Univ.subst_instance_constraints u (Univ.UContext.constraints mib.mind_universes)
+    Univ.subst_instance_constraints u (Univ.UContext.constraints (Univ.UInfoInd.univ_context mib.mind_universes))
   else Univ.Constraint.empty
 
 
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index f5e8e8653..1568fe0bf 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -429,7 +429,7 @@ let globalize_mind_universes mb =
   if mb.mind_polymorphic then
     [Now (true, Univ.ContextSet.empty)]
   else
-    [Now (false, Univ.ContextSet.of_context mb.mind_universes)]
+    [Now (false, Univ.ContextSet.of_context (Univ.UInfoInd.univ_context mb.mind_universes))]
 
 let constraints_of_sfb env sfb = 
   match sfb with
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index bdfd00a8d..3cf2299d8 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -313,7 +313,7 @@ let infer_declaration ~trust env kn dcl =
     in
     let term, typ = pb.proj_eta in
       Def (Mod_subst.from_val (hcons_constr term)), RegularArity typ, Some pb,
-      mib.mind_polymorphic, mib.mind_universes, false, None
+      mib.mind_polymorphic, Univ.UInfoInd.univ_context mib.mind_universes, false, None
 
 let global_vars_set_constant_type env = function
   | RegularArity t -> global_vars_set env t
diff --git a/kernel/univ.ml b/kernel/univ.ml
index e8b9ae33a..f124bb39e 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -1053,14 +1053,14 @@ struct
     let len = Array.length (Instance.to_array ctx) in
     let halflen = len / 2 in
     (Instance.of_array (Array.sub (Instance.to_array ctx) 0 halflen),
-     Instance.of_array (Array.sub (Instance.to_array ctx) halflen len))
+     Instance.of_array (Array.sub (Instance.to_array ctx) halflen halflen))
 
   let pr prl (univcst, subtypcst) =
     if UContext.is_empty univcst then mt() else
       let (ctx, ctx') = halve_context (UContext.instance subtypcst) in
-      (UContext.pr prl univcst) ++
-      h 0 (str "~@{" ++ Instance.pr prl ctx ++ str "} <= ~@{" ++ Instance.pr prl ctx' ++ str "}")
-           ++ h 0 (v 0 (Constraint.pr prl (UContext.constraints subtypcst)))
+      (UContext.pr prl univcst) ++ fnl () ++ fnl () ++
+        h 0 (str "~@{" ++ Instance.pr prl ctx ++ str "} <= ~@{" ++ Instance.pr prl ctx' ++ str "} iff ")
+         ++ fnl () ++ h 0 (v 0 (Constraint.pr prl (UContext.constraints subtypcst)))
 
   let hcons (univcst, subtypcst) =
     (UContext.hcons univcst, UContext.hcons subtypcst)
diff --git a/kernel/vconv.ml b/kernel/vconv.ml
index 74d956bef..fa1662270 100644
--- a/kernel/vconv.ml
+++ b/kernel/vconv.ml
@@ -93,7 +93,7 @@ and conv_atom env pb k a1 stk1 a2 stk2 cu =
         if Environ.polymorphic_ind ind1 env
         then
           let mib = Environ.lookup_mind mi env in
-	  let ulen = Univ.UContext.size mib.Declarations.mind_universes in
+	  let ulen = Univ.UContext.size (Univ.UInfoInd.univ_context mib.Declarations.mind_universes) in
           match stk1 , stk2 with
 	  | [], [] -> assert (Int.equal ulen 0); cu
 	  | Zapp args1 :: stk1' , Zapp args2 :: stk2' ->
diff --git a/library/declare.ml b/library/declare.ml
index 06eeeeab5..f3150174c 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -352,7 +352,7 @@ let dummy_inductive_entry (_,m) = ([],{
   mind_entry_finite = Decl_kinds.BiFinite;
   mind_entry_inds = List.map dummy_one_inductive_entry m.mind_entry_inds;
   mind_entry_polymorphic = false;
-  mind_entry_universes = (Univ.UContext.empty, Univ.UContext.empty);
+  mind_entry_universes = Univ.UInfoInd.empty;
   mind_entry_private = None;
 })
 
diff --git a/library/global.ml b/library/global.ml
index 1ba86699d..a45998384 100644
--- a/library/global.ml
+++ b/library/global.ml
@@ -178,13 +178,13 @@ let type_of_global_unsafe r =
      let (mib, oib as specif) = Inductive.lookup_mind_specif env ind in
      let inst = 
        if mib.Declarations.mind_polymorphic then 
-	 Univ.UContext.instance mib.Declarations.mind_universes
+	 Univ.UContext.instance (Univ.UInfoInd.univ_context mib.Declarations.mind_universes)
        else Univ.Instance.empty
      in
        Inductive.type_of_inductive env (specif, inst)
   | ConstructRef cstr ->
      let (mib,oib as specif) = Inductive.lookup_mind_specif env (inductive_of_constructor cstr) in
-     let inst = Univ.UContext.instance mib.Declarations.mind_universes in
+     let inst = Univ.UContext.instance (Univ.UInfoInd.univ_context mib.Declarations.mind_universes) in
        Inductive.type_of_constructor (cstr,inst) specif
 
 let type_of_global_in_context env r = 
@@ -200,13 +200,13 @@ let type_of_global_in_context env r =
   | IndRef ind ->
      let (mib, oib as specif) = Inductive.lookup_mind_specif env ind in
      let univs = 
-       if mib.mind_polymorphic then Univ.instantiate_univ_context mib.mind_universes 
+       if mib.mind_polymorphic then Univ.instantiate_univ_context (Univ.UInfoInd.univ_context mib.mind_universes)
        else Univ.UContext.empty
      in Inductive.type_of_inductive env (specif, Univ.UContext.instance univs), univs
   | ConstructRef cstr ->
      let (mib,oib as specif) = Inductive.lookup_mind_specif env (inductive_of_constructor cstr) in
      let univs = 
-       if mib.mind_polymorphic then Univ.instantiate_univ_context mib.mind_universes 
+       if mib.mind_polymorphic then Univ.instantiate_univ_context (Univ.UInfoInd.univ_context mib.mind_universes)
        else Univ.UContext.empty
      in
      let inst = Univ.UContext.instance univs in
@@ -222,10 +222,10 @@ let universes_of_global env r =
           (Environ.opaque_tables env) cb
     | IndRef ind ->
       let (mib, oib) = Inductive.lookup_mind_specif env ind in
-	Univ.instantiate_univ_context mib.mind_universes 
+	Univ.instantiate_univ_context (Univ.UInfoInd.univ_context mib.mind_universes)
     | ConstructRef cstr ->
       let (mib,oib) = Inductive.lookup_mind_specif env (inductive_of_constructor cstr) in
-	Univ.instantiate_univ_context mib.mind_universes 
+	Univ.instantiate_univ_context (Univ.UInfoInd.univ_context mib.mind_universes)
 
 let universes_of_global gr = 
   universes_of_global (env ()) gr
diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml
index d7b484281..152ccb079 100644
--- a/pretyping/typeclasses.ml
+++ b/pretyping/typeclasses.ml
@@ -123,7 +123,7 @@ let typeclass_univ_instance (cl,u') =
 	  else Univ.Instance.empty
       | IndRef c ->
          let mib,oib = Global.lookup_inductive c in
-	  if mib.mind_polymorphic then Univ.UContext.instance mib.mind_universes
+	  if mib.mind_polymorphic then Univ.UContext.instance (Univ.UInfoInd.univ_context mib.mind_universes)
 	  else Univ.Instance.empty
       | _ -> Univ.Instance.empty
     in Array.fold_left2 (fun subst u u' -> Univ.LMap.add u u' subst) 
diff --git a/pretyping/vnorm.ml b/pretyping/vnorm.ml
index b08666483..074b7373c 100644
--- a/pretyping/vnorm.ml
+++ b/pretyping/vnorm.ml
@@ -174,7 +174,7 @@ and nf_whd env sigma whd typ =
   | Vatom_stk(Aind ((mi,i) as ind), stk) ->
      let mib = Environ.lookup_mind mi env in
      let nb_univs =
-       if mib.mind_polymorphic then Univ.UContext.size mib.mind_universes
+       if mib.mind_polymorphic then Univ.UContext.size (Univ.UInfoInd.univ_context mib.mind_universes)
        else 0
      in
      let mk u =
diff --git a/printing/printer.ml b/printing/printer.ml
index d6f0778f7..c27a9b009 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -261,6 +261,13 @@ let pr_universe_ctx sigma c =
   else
     mt()
 
+let pr_universe_info_ind sigma uii =
+  if !Detyping.print_universes && not (Univ.UInfoInd.is_empty uii) then
+    fnl()++pr_in_comment (fun uii -> v 0
+      (Univ.pr_universe_info_ind (Termops.pr_evd_level sigma) uii)) uii
+  else
+    mt()
+
 (**********************************************************************)
 (* Global references *)
 
diff --git a/printing/printer.mli b/printing/printer.mli
index 3fce06561..6531036a1 100644
--- a/printing/printer.mli
+++ b/printing/printer.mli
@@ -97,6 +97,7 @@ val pr_sort                : evar_map -> sorts -> std_ppcmds
 val pr_polymorphic         : bool -> std_ppcmds
 val pr_universe_instance   : evar_map -> Univ.universe_context -> std_ppcmds
 val pr_universe_ctx        : evar_map -> Univ.universe_context -> std_ppcmds
+val pr_universe_info_ind   : evar_map -> Univ.universe_info_ind -> std_ppcmds
 
 (** Printing global references using names as short as possible *)
 
diff --git a/printing/printmod.ml b/printing/printmod.ml
index c4affd4ac..7dc47a4a4 100644
--- a/printing/printmod.ml
+++ b/printing/printmod.ml
@@ -89,7 +89,7 @@ let build_ind_type env mip =
 
 let print_one_inductive env sigma mib ((_,i) as ind) =
   let u = if mib.mind_polymorphic then 
-      Univ.UContext.instance mib.mind_universes 
+      Univ.UContext.instance (Univ.UInfoInd.univ_context mib.mind_universes)
     else Univ.Instance.empty in
   let mip = mib.mind_packets.(i) in
   let params = Inductive.inductive_paramdecls (mib,u) in
@@ -100,7 +100,7 @@ let print_one_inductive env sigma mib ((_,i) as ind) =
   let envpar = push_rel_context params env in
   let inst =
     if mib.mind_polymorphic then
-      Printer.pr_universe_instance sigma mib.mind_universes
+      Printer.pr_universe_instance sigma (Univ.UInfoInd.univ_context mib.mind_universes)
     else mt ()
   in
   hov 0 (
@@ -124,7 +124,7 @@ let print_mutual_inductive env mind mib =
     def keyword ++ spc () ++
     prlist_with_sep (fun () -> fnl () ++ str"  with ")
       (print_one_inductive env sigma mib) inds ++
-      Printer.pr_universe_ctx sigma (Univ.instantiate_univ_context mib.mind_universes))
+      Printer.pr_universe_info_ind sigma (Univ.instantiate_univ_info_ind mib.mind_universes))
 
 let get_fields =
   let rec prodec_rec l subst c =
@@ -142,7 +142,7 @@ let get_fields =
 let print_record env mind mib =
   let u = 
     if mib.mind_polymorphic then 
-      Univ.UContext.instance mib.mind_universes 
+      Univ.UContext.instance (Univ.UInfoInd.univ_context mib.mind_universes)
     else Univ.Instance.empty 
   in
   let mip = mib.mind_packets.(0) in
@@ -175,7 +175,7 @@ let print_record env mind mib =
         (fun (id,b,c) ->
           pr_id id ++ str (if b then " : " else " := ") ++
           Printer.pr_lconstr_env envpar sigma c) fields) ++ str" }" ++
-      Printer.pr_universe_ctx sigma (Univ.instantiate_univ_context mib.mind_universes))
+      Printer.pr_universe_info_ind sigma (Univ.instantiate_univ_info_ind mib.mind_universes))
 
 let pr_mutual_inductive_body env mind mib =
   if mib.mind_record <> None && not !Flags.raw_print then
diff --git a/vernac/command.ml b/vernac/command.ml
index 5f95a42a3..b76c2247b 100644
--- a/vernac/command.ml
+++ b/vernac/command.ml
@@ -656,7 +656,7 @@ let interp_mutual_inductive (paramsl,indl) notations poly prv finite =
     mind_entry_inds = entries;
     mind_entry_polymorphic = poly;
     mind_entry_private = if prv then Some false else None;
-    mind_entry_universes = (uctx, Univ.UContext.empty);
+    mind_entry_universes = Universes.univ_inf_ind_from_universe_context uctx;
   },
     pl, impls
 
diff --git a/vernac/discharge.ml b/vernac/discharge.ml
index 9c70eb97e..91e126ef1 100644
--- a/vernac/discharge.ml
+++ b/vernac/discharge.ml
@@ -81,17 +81,10 @@ let process_inductive (sechyps,abs_ctx) modlist mib =
   let nparams = mib.mind_nparams in
   let subst, univs = 
     if mib.mind_polymorphic then 
-      let inst = Univ.UContext.instance mib.mind_universes in
-      let cstrs = Univ.UContext.constraints mib.mind_universes in
+      let inst = Univ.UContext.instance (Univ.UInfoInd.univ_context mib.mind_universes) in
+      let cstrs = Univ.UContext.constraints (Univ.UInfoInd.univ_context mib.mind_universes) in
 	inst, Univ.UContext.make (inst, Univ.subst_instance_constraints inst cstrs)
-    else Univ.Instance.empty, mib.mind_universes
-  in
-  let substsbt, univssbt = 
-    if mib.mind_polymorphic then 
-      let inst = Univ.UContext.instance mib.mind_subtyping in
-      let cstrs = Univ.UContext.constraints mib.mind_subtyping in
-	inst, Univ.UContext.make (inst, Univ.subst_instance_constraints inst cstrs)
-    else Univ.Instance.empty, Univ.UContext.empty
+    else Univ.Instance.empty, (Univ.UInfoInd.univ_context mib.mind_universes)
   in
   let inds =
     Array.map_to_list
@@ -112,6 +105,7 @@ let process_inductive (sechyps,abs_ctx) modlist mib =
   let (params',inds') = abstract_inductive sechyps' nparams inds in
   let abs_ctx = Univ.instantiate_univ_context abs_ctx in
   let univs = Univ.UContext.union abs_ctx univs in
+  let univ_info_ind = Universes.univ_inf_ind_from_universe_context univs in (* Here we must re-infer subtyping constraints. For now we just revert to trivial subtyping. *)
   let record = match mib.mind_record with
     | Some (Some (id, _, _)) -> Some (Some id)
     | Some None -> Some None
@@ -123,5 +117,5 @@ let process_inductive (sechyps,abs_ctx) modlist mib =
     mind_entry_inds = inds';
     mind_entry_polymorphic = mib.mind_polymorphic;
     mind_entry_private = mib.mind_private;
-    mind_entry_universes = (univs, univssbt);
+    mind_entry_universes = univ_info_ind
   }
diff --git a/vernac/record.ml b/vernac/record.ml
index 5c76bb4b2..64f5e81d4 100644
--- a/vernac/record.ml
+++ b/vernac/record.ml
@@ -268,7 +268,7 @@ let declare_projections indsp ?(kind=StructureComponent) binder_name coers field
   let u = Declareops.inductive_instance mib in
   let paramdecls = Inductive.inductive_paramdecls (mib, u) in
   let poly = mib.mind_polymorphic in
-  let ctx = Univ.instantiate_univ_context mib.mind_universes in
+  let ctx = Univ.instantiate_univ_context (Univ.UInfoInd.univ_context mib.mind_universes) in
   let indu = indsp, u in
   let r = mkIndU (indsp,u) in
   let rp = applist (r, Context.Rel.to_extended_list mkRel 0 paramdecls) in
@@ -466,7 +466,7 @@ let declare_class finite def poly ctx id idbuild paramimpls params arity
       in
       cref, [Name proj_name, sub, Some proj_cst]
     | _ ->
-       let ind = declare_structure BiFinite poly (ctx, Univ.UContext.empty) (snd id) idbuild paramimpls
+       let ind = declare_structure BiFinite poly (Universes.univ_inf_ind_from_universe_context ctx) (snd id) idbuild paramimpls
 	  params arity template fieldimpls fields
 	  ~kind:Method ~name:binder_name false (List.map (fun _ -> false) fields) sign
        in
@@ -515,7 +515,7 @@ let add_inductive_class ind =
   let mind, oneind = Global.lookup_inductive ind in
   let k =
     let ctx = oneind.mind_arity_ctxt in
-    let inst = Univ.UContext.instance mind.mind_universes in
+    let inst = Univ.UContext.instance (Univ.UInfoInd.univ_context mind.mind_universes) in
     let ty = Inductive.type_of_inductive
       (push_rel_context ctx (Global.env ()))
       ((mind,oneind),inst)
@@ -571,7 +571,7 @@ let definition_structure (kind,poly,finite,(is_coe,((loc,idstruc),pl)),ps,cfs,id
 	let implfs = List.map
 	  (fun impls -> implpars @ Impargs.lift_implicits
 	    (succ (List.length params)) impls) implfs in
-	let ind = declare_structure finite poly (ctx, Univ.UContext.empty) idstruc
+	let ind = declare_structure finite poly (Universes.univ_inf_ind_from_universe_context ctx) idstruc
 	  idbuild implpars params arity template implfs 
 	  fields is_coe (List.map (fun coe -> not (Option.is_empty coe)) coers) sign in
 	IndRef ind
diff --git a/vernac/record.mli b/vernac/record.mli
index a380b041a..ec5d2cf83 100644
--- a/vernac/record.mli
+++ b/vernac/record.mli
@@ -27,7 +27,7 @@ val declare_projections :
 val declare_structure :
   Decl_kinds.recursivity_kind ->
   bool (** polymorphic?*) ->
-  (Univ.universe_context * Univ.universe_context) (** universe and subtyping constraints *) ->
+  Univ.universe_info_ind (** universe and subtyping constraints *) ->
   Id.t -> Id.t ->
   manual_explicitation list -> Context.Rel.t -> (** params *) constr -> (** arity *)
   bool (** template arity ? *) ->