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.

4 files changed, 11 insertions, 17 deletions

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 ? *) ->