Clean up universes of constants and inductives

9 files changed, 80 insertions, 38 deletions

diff --git a/vernac/command.ml b/vernac/command.ml
index 2345cb4c5..406477356 100644
--- a/vernac/command.ml
+++ b/vernac/command.ml
@@ -649,20 +649,25 @@ let interp_mutual_inductive (paramsl,indl) notations cum poly prv finite =
 	indimpls, List.map (fun impls ->
 	  userimpls @ (lift_implicits len impls)) cimpls) indimpls constructors
   in
-  let ground_uinfind = Universes.univ_inf_ind_from_universe_context uctx in
+  let univs =
+    if poly then
+      if cum then
+        Cumulative_ind_entry (Universes.univ_inf_ind_from_universe_context uctx)
+      else Polymorphic_ind_entry uctx
+    else
+      Monomorphic_ind_entry uctx
+  in
   (* Build the mutual inductive entry *)
-  let mind_ent = 
+  let mind_ent =
     { mind_entry_params = List.map prepare_param ctx_params;
       mind_entry_record = None;
       mind_entry_finite = finite;
       mind_entry_inds = entries;
-      mind_entry_polymorphic = poly;
-      mind_entry_cumulative = cum;
       mind_entry_private = if prv then Some false else None;
-      mind_entry_universes = ground_uinfind;
+      mind_entry_universes = univs;
     }
   in
-  (if poly then
+  (if poly && cum then
       Inductiveops.infer_inductive_subtyping env_ar evd mind_ent
    else mind_ent), pl, impls
 
diff --git a/vernac/discharge.ml b/vernac/discharge.ml
index 738e27f63..18f93334b 100644
--- a/vernac/discharge.ml
+++ b/vernac/discharge.ml
@@ -79,12 +79,14 @@ let refresh_polymorphic_type_of_inductive (_,mip) =
 
 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 (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, (Univ.UInfoInd.univ_context mib.mind_universes)
+  let subst, univs =
+    match mib.mind_universes with
+    | Monomorphic_ind ctx -> Univ.Instance.empty, ctx
+    | Polymorphic_ind auctx ->
+      Univ.AUContext.instance auctx, Univ.instantiate_univ_context auctx
+    | Cumulative_ind cumi ->
+      let auctx = Univ.ACumulativityInfo.univ_context cumi in
+      Univ.AUContext.instance auctx, Univ.instantiate_univ_context auctx
   in
   let inds =
     Array.map_to_list
@@ -105,7 +107,12 @@ 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
+  let ind_univs =
+    match mib.mind_universes with
+    | Monomorphic_ind _ -> Monomorphic_ind_entry univs
+    | Polymorphic_ind _ -> Polymorphic_ind_entry univs
+    | Cumulative_ind _ ->
+      Cumulative_ind_entry (Universes.univ_inf_ind_from_universe_context univs) in
   let record = match mib.mind_record with
     | Some (Some (id, _, _)) -> Some (Some id)
     | Some None -> Some None
@@ -115,9 +122,7 @@ let process_inductive (sechyps,abs_ctx) modlist mib =
     mind_entry_finite = mib.mind_finite;
     mind_entry_params = params';
     mind_entry_inds = inds';
-    mind_entry_polymorphic = mib.mind_polymorphic;
-    mind_entry_cumulative = mib.mind_cumulative;
     mind_entry_private = mib.mind_private;
-    mind_entry_universes = univ_info_ind
+    mind_entry_universes = ind_univs
   }
 
diff --git a/vernac/discharge.mli b/vernac/discharge.mli
index 18d1b6776..3845c04a1 100644
--- a/vernac/discharge.mli
+++ b/vernac/discharge.mli
@@ -11,4 +11,5 @@ open Entries
 open Opaqueproof
 
 val process_inductive :
-  Context.Named.t Univ.in_universe_context -> work_list -> mutual_inductive_body -> mutual_inductive_entry
+  ((Term.constr, Term.constr) Context.Named.pt * Univ.abstract_universe_context)
+  -> work_list -> mutual_inductive_body -> mutual_inductive_entry
diff --git a/vernac/himsg.ml b/vernac/himsg.ml
index 6d8dd82ac..ce91e1a09 100644
--- a/vernac/himsg.ml
+++ b/vernac/himsg.ml
@@ -889,6 +889,10 @@ let explain_not_match_error = function
   | NoTypeConstraintExpected ->
     strbrk "a definition whose type is constrained can only be subtype " ++
     strbrk "of a definition whose type is itself constrained"
+  | CumulativeStatusExpected b ->
+    let status b = if b then str"cumulative" else str"non-cumulative" in
+      str "a " ++ status b ++ str" declaration was expected, but a " ++ 
+	status (not b) ++ str" declaration was found"
   | PolymorphicStatusExpected b ->
     let status b = if b then str"polymorphic" else str"monomorphic" in
       str "a " ++ status b ++ str" declaration was expected, but a " ++ 
diff --git a/vernac/ind_tables.ml b/vernac/ind_tables.ml
index f3259f1f3..65d42b626 100644
--- a/vernac/ind_tables.ml
+++ b/vernac/ind_tables.ml
@@ -148,7 +148,7 @@ let define_individual_scheme_base kind suff f mode idopt (mind,i as ind) =
   let id = match idopt with
     | Some id -> id
     | None -> add_suffix mib.mind_packets.(i).mind_typename suff in
-  let const = define mode id c mib.mind_polymorphic ctx in
+  let const = define mode id c (Declareops.inductive_is_polymorphic mib) ctx in
   declare_scheme kind [|ind,const|];
   const, Safe_typing.add_private
      (Safe_typing.private_con_of_scheme ~kind (Global.safe_env()) [ind,const]) eff
@@ -166,7 +166,7 @@ let define_mutual_scheme_base kind suff f mode names mind =
       try Int.List.assoc i names
       with Not_found -> add_suffix mib.mind_packets.(i).mind_typename suff) in
   let consts = Array.map2 (fun id cl -> 
-     define mode id cl mib.mind_polymorphic ctx) ids cl in
+     define mode id cl (Declareops.inductive_is_polymorphic mib) ctx) ids cl in
   let schemes = Array.mapi (fun i cst -> ((mind,i),cst)) consts in
   declare_scheme kind schemes;
   consts,
diff --git a/vernac/obligations.ml b/vernac/obligations.ml
index e03e9b803..135e4c63a 100644
--- a/vernac/obligations.ml
+++ b/vernac/obligations.ml
@@ -365,8 +365,8 @@ let get_body obl =
   match obl.obl_body with
   | None -> None
   | Some (DefinedObl c) ->
-    let ctx = Environ.constant_context (Global.env ()) c in
-    let pc = (c, Univ.UContext.instance ctx) in
+    let u = Environ.constant_instance (Global.env ()) c in
+    let pc = (c, u) in
       Some (DefinedObl pc)
   | Some (TermObl c) ->
       Some (TermObl c)
diff --git a/vernac/record.ml b/vernac/record.ml
index b95131b72..7dd70d013 100644
--- a/vernac/record.ml
+++ b/vernac/record.ml
@@ -265,10 +265,16 @@ let warn_non_primitive_record =
 let declare_projections indsp ?(kind=StructureComponent) binder_name coers fieldimpls fields =
   let env = Global.env() in
   let (mib,mip) = Global.lookup_inductive indsp in
-  let u = Declareops.inductive_instance mib in
+  let u = Declareops.inductive_polymorphic_instance mib in
   let paramdecls = Inductive.inductive_paramdecls (mib, u) in
-  let poly = mib.mind_polymorphic in
-  let ctx = Univ.instantiate_univ_context (Univ.UInfoInd.univ_context mib.mind_universes) in
+  let poly = Declareops.inductive_is_polymorphic mib in
+  let ctx =
+    match mib.mind_universes with
+    | Monomorphic_ind ctx -> ctx
+    | Polymorphic_ind auctx -> Univ.instantiate_univ_context auctx
+    | Cumulative_ind cumi -> 
+      Univ.instantiate_univ_context (Univ.ACumulativityInfo.univ_context cumi)
+  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
@@ -377,12 +383,18 @@ let structure_signature ctx =
 
 open Typeclasses
 
-let declare_structure finite cum poly ctx id idbuild paramimpls params arity template 
+let declare_structure finite univs id idbuild paramimpls params arity template 
     fieldimpls fields ?(kind=StructureComponent) ?name is_coe coers sign =
   let nparams = List.length params and nfields = List.length fields in
   let args = Context.Rel.to_extended_list mkRel nfields params in
   let ind = applist (mkRel (1+nparams+nfields), args) in
   let type_constructor = it_mkProd_or_LetIn ind fields in
+  let poly, ctx =
+    match univs with
+    | Monomorphic_ind_entry ctx -> false, ctx
+    | Polymorphic_ind_entry ctx -> true, ctx
+    | Cumulative_ind_entry cumi -> true, (Univ.CumulativityInfo.univ_context cumi)
+  in
   let binder_name = 
     match name with
     | None -> Id.of_string (Unicode.lowercase_first_char (Id.to_string id)) 
@@ -400,17 +412,15 @@ let declare_structure finite cum poly ctx id idbuild paramimpls params arity tem
       mind_entry_record = Some (if !primitive_flag then Some binder_name else None);
       mind_entry_finite = finite;
       mind_entry_inds = [mie_ind];
-      mind_entry_polymorphic = poly;
-      mind_entry_cumulative = cum;
       mind_entry_private = None;
-      mind_entry_universes = ctx;
+      mind_entry_universes = univs;
     }
   in
   let mie =
     if poly then
       begin
         let env = Global.env () in
-        let env' = Environ.push_context (Univ.UInfoInd.univ_context ctx) env in
+        let env' = Environ.push_context ctx env in
         (* let env'' = Environ.push_rel_context params env' in *)
         let evd = Evd.from_env env' in
         Inductiveops.infer_inductive_subtyping env' evd mie
@@ -479,7 +489,16 @@ let declare_class finite def cum poly ctx id idbuild paramimpls params arity
       in
       cref, [Name proj_name, sub, Some proj_cst]
     | _ ->
-       let ind = declare_structure BiFinite cum poly (Universes.univ_inf_ind_from_universe_context ctx) (snd id) idbuild paramimpls
+       let univs =
+         if poly then
+           if cum then
+             Cumulative_ind_entry (Universes.univ_inf_ind_from_universe_context ctx)
+           else
+             Polymorphic_ind_entry ctx
+         else
+           Monomorphic_ind_entry ctx
+       in
+       let ind = declare_structure BiFinite univs (snd id) idbuild paramimpls
 	  params arity template fieldimpls fields
 	  ~kind:Method ~name:binder_name false (List.map (fun _ -> false) fields) sign
        in
@@ -528,7 +547,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 (Univ.UInfoInd.univ_context mind.mind_universes) in
+    let inst = Declareops.inductive_polymorphic_instance mind in
     let ty = Inductive.type_of_inductive
       (push_rel_context ctx (Global.env ()))
       ((mind,oneind),inst)
@@ -581,10 +600,20 @@ let definition_structure (kind,cum,poly,finite,(is_coe,((loc,idstruc),pl)),ps,cf
 	  implpars params arity template implfs fields is_coe coers priorities sign in
 	gr
     | _ ->
-	let implfs = List.map
+      let implfs = List.map
 	  (fun impls -> implpars @ Impargs.lift_implicits
-	    (succ (List.length params)) impls) implfs in
-	let ind = declare_structure finite cum poly (Universes.univ_inf_ind_from_universe_context ctx) idstruc
+	           (succ (List.length params)) impls) implfs 
+      in
+      let univs =
+        if poly then
+          if cum then
+            Cumulative_ind_entry (Universes.univ_inf_ind_from_universe_context ctx)
+          else
+            Polymorphic_ind_entry ctx
+        else
+          Monomorphic_ind_entry ctx
+      in
+      let ind = declare_structure finite univs 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 c43d833b0..aa530fd61 100644
--- a/vernac/record.mli
+++ b/vernac/record.mli
@@ -26,9 +26,7 @@ val declare_projections :
 
 val declare_structure :
   Decl_kinds.recursivity_kind ->
-  Decl_kinds.cumulative_inductive_flag ->
-  Decl_kinds.polymorphic ->
-  Univ.universe_info_ind (** universe and subtyping constraints *) ->
+  Entries.inductive_universes ->
   Id.t -> Id.t ->
   manual_explicitation list -> Context.Rel.t -> (** params *) constr -> (** arity *)
   bool (** template arity ? *) ->
diff --git a/vernac/search.ml b/vernac/search.ml
index 0ff78f439..5e56ada8a 100644
--- a/vernac/search.ml
+++ b/vernac/search.ml
@@ -85,7 +85,7 @@ let iter_declarations (fn : global_reference -> env -> constr -> unit) =
     let mib = Global.lookup_mind mind in
     let iter_packet i mip =
       let ind = (mind, i) in
-      let u = Declareops.inductive_instance mib in
+      let u = Declareops.inductive_polymorphic_instance mib in
       let i = (ind, u) in
       let typ = Inductiveops.type_of_inductive env i in
       let () = fn (IndRef ind) env typ in