Clean up universes of constants and inductives

5 files changed, 45 insertions, 43 deletions

diff --git a/library/declare.ml b/library/declare.ml
index e2b726f45..db3dbcbd9 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -158,7 +158,7 @@ let cache_constant ((sp,kn), obj) =
   assert (eq_constant kn' (constant_of_kn kn));
   Nametab.push (Nametab.Until 1) sp (ConstRef (constant_of_kn kn));
   let cst = Global.lookup_constant kn' in
-  add_section_constant cst.const_polymorphic kn' cst.const_hyps;
+  add_section_constant (Declareops.constant_is_polymorphic cst) kn' cst.const_hyps;
   Dischargedhypsmap.set_discharged_hyps sp obj.cst_hyps;
   add_constant_kind (constant_of_kn kn) obj.cst_kind
 
@@ -325,7 +325,7 @@ let cache_inductive ((sp,kn),(dhyps,mie)) =
   let kn' = Global.add_mind dir id mie in
   assert (eq_mind kn' (mind_of_kn kn));
   let mind = Global.lookup_mind kn' in
-  add_section_kn mind.mind_polymorphic kn' mind.mind_hyps;
+  add_section_kn (Declareops.inductive_is_polymorphic mind) kn' mind.mind_hyps;
   Dischargedhypsmap.set_discharged_hyps sp dhyps;
   List.iter (fun (sp, ref) -> Nametab.push (Nametab.Until 1) sp ref) names
 
@@ -351,25 +351,26 @@ let dummy_inductive_entry (_,m) = ([],{
   mind_entry_record = None;
   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_cumulative = false;
-  mind_entry_universes = Univ.UInfoInd.empty;
+  mind_entry_universes = Monomorphic_ind_entry Univ.UContext.empty;
   mind_entry_private = None;
 })
 
 (* reinfer subtyping constraints for inductive after section is dischared. *)
-let infer_inductive_subtyping (pth, mind_ent) = 
-  if mind_ent.mind_entry_polymorphic && mind_ent.mind_entry_cumulative then
+let infer_inductive_subtyping (pth, mind_ent) =
+  match mind_ent.mind_entry_universes with
+  | Monomorphic_ind_entry _ | Polymorphic_ind_entry _ ->
+    (pth, mind_ent)
+  | Cumulative_ind_entry cumi ->
     begin
       let env = Global.env () in
       let env' =
-        Environ.push_context (Univ.UInfoInd.univ_context mind_ent.mind_entry_universes) env
+        Environ.push_context
+          (Univ.CumulativityInfo.univ_context cumi) env
       in
       (* let (env'', typed_params) = Typeops.infer_local_decls env' (mind_ent.mind_entry_params) in *)
       let evd = Evd.from_env env' in
         (pth, Inductiveops.infer_inductive_subtyping env' evd mind_ent)
     end
-  else (pth, mind_ent)
 
 type inductive_obj = Dischargedhypsmap.discharged_hyps * mutual_inductive_entry
 
diff --git a/library/global.ml b/library/global.ml
index a45998384..6d80012f4 100644
--- a/library/global.ml
+++ b/library/global.ml
@@ -176,19 +176,14 @@ let type_of_global_unsafe r =
        Vars.subst_instance_constr (Univ.UContext.instance univs) ty
   | IndRef ind ->
      let (mib, oib as specif) = Inductive.lookup_mind_specif env ind in
-     let inst = 
-       if mib.Declarations.mind_polymorphic then 
-	 Univ.UContext.instance (Univ.UInfoInd.univ_context mib.Declarations.mind_universes)
-       else Univ.Instance.empty
-     in
+     let inst = Declareops.inductive_polymorphic_instance mib 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 (Univ.UInfoInd.univ_context mib.Declarations.mind_universes) in
-       Inductive.type_of_constructor (cstr,inst) specif
+     let inst = Declareops.inductive_polymorphic_instance mib in
+     Inductive.type_of_constructor (cstr,inst) specif
 
 let type_of_global_in_context env r = 
-  let open Declarations in
   match r with
   | VarRef id -> Environ.named_type id env, Univ.UContext.empty
   | ConstRef c -> 
@@ -199,21 +194,17 @@ let type_of_global_in_context env r =
        Typeops.type_of_constant_type env cb.Declarations.const_type, univs
   | 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 (Univ.UInfoInd.univ_context mib.mind_universes)
-       else Univ.UContext.empty
-     in Inductive.type_of_inductive env (specif, Univ.UContext.instance univs), univs
+     let univs = Declareops.inductive_polymorphic_context mib 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 (Univ.UInfoInd.univ_context mib.mind_universes)
-       else Univ.UContext.empty
-     in
-     let inst = Univ.UContext.instance univs in
-       Inductive.type_of_constructor (cstr,inst) specif, univs
+    let (mib,oib as specif) =
+      Inductive.lookup_mind_specif env (inductive_of_constructor cstr) 
+    in
+    let univs = Declareops.inductive_polymorphic_context mib in
+    let inst = Univ.UContext.instance univs in
+    Inductive.type_of_constructor (cstr,inst) specif, univs
 
 let universes_of_global env r = 
-  let open Declarations in
     match r with
     | VarRef id -> Univ.UContext.empty
     | ConstRef c -> 
@@ -222,10 +213,11 @@ 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 (Univ.UInfoInd.univ_context mib.mind_universes)
+      Declareops.inductive_polymorphic_context mib
     | ConstructRef cstr ->
-      let (mib,oib) = Inductive.lookup_mind_specif env (inductive_of_constructor cstr) in
-	Univ.instantiate_univ_context (Univ.UInfoInd.univ_context mib.mind_universes)
+      let (mib,oib) = 
+        Inductive.lookup_mind_specif env (inductive_of_constructor cstr) in
+      Declareops.inductive_polymorphic_context mib
 
 let universes_of_global gr = 
   universes_of_global (env ()) gr
diff --git a/library/lib.ml b/library/lib.ml
index f22f53ead..8127316d7 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -402,7 +402,7 @@ let find_opening_node id =
 type variable_info = Context.Named.Declaration.t * Decl_kinds.binding_kind
 
 type variable_context = variable_info list
-type abstr_info = variable_context * Univ.universe_level_subst * Univ.UContext.t
+type abstr_info = variable_context * Univ.universe_level_subst * Univ.AUContext.t
 		  
 type abstr_list = abstr_info Names.Cmap.t * abstr_info Names.Mindmap.t
 
@@ -465,9 +465,9 @@ let add_section_replacement f g poly hyps =
     let () = check_same_poly poly vars in
     let sechyps,ctx = extract_hyps (vars,hyps) in
     let ctx = Univ.ContextSet.to_context ctx in
-    let subst, ctx = Univ.abstract_universes true ctx in
+    let subst, ctx = Univ.abstract_universes ctx in
     let args = instance_from_variable_context (List.rev sechyps) in
-    sectab := (vars,f (Univ.UContext.instance ctx,args) exps,
+    sectab := (vars,f (Univ.AUContext.instance ctx,args) exps,
 	      g (sechyps,subst,ctx) abs)::sl
 
 let add_section_kn poly kn =
diff --git a/library/lib.mli b/library/lib.mli
index f47d6e1a5..284d33980 100644
--- a/library/lib.mli
+++ b/library/lib.mli
@@ -157,7 +157,7 @@ val xml_close_section : (Names.Id.t -> unit) Hook.t
 (** {6 Section management for discharge } *)
 type variable_info = Context.Named.Declaration.t * Decl_kinds.binding_kind
 type variable_context = variable_info list 
-type abstr_info = variable_context * Univ.universe_level_subst * Univ.UContext.t
+type abstr_info = variable_context * Univ.universe_level_subst * Univ.AUContext.t
 
 val instance_from_variable_context : variable_context -> Names.Id.t array
 val named_of_variable_context : variable_context -> Context.Named.t
diff --git a/library/univops.ml b/library/univops.ml
index e9383c6d9..60c12f0d8 100644
--- a/library/univops.ml
+++ b/library/univops.ml
@@ -22,9 +22,8 @@ let universes_of_constr c =
   in aux LSet.empty c
 
 let universes_of_inductive mind =
-  if mind.mind_polymorphic then
-  begin
-    let u = Univ.UContext.instance (Univ.UInfoInd.univ_context mind.mind_universes) in
+  let process auctx =
+    let u = Univ.AUContext.instance auctx in
     let univ_of_one_ind oind = 
       let arity_univs =
         Context.Rel.fold_outside
@@ -43,12 +42,22 @@ let universes_of_inductive mind =
           Univ.LSet.union (universes_of_constr cns) unvs) arity_univs 
        oind.mind_nf_lc
     in
-    let univs = Array.fold_left (fun unvs pk -> Univ.LSet.union (univ_of_one_ind pk) unvs) Univ.LSet.empty mind.mind_packets in
-    let mindcnt = Univ.UContext.constraints (Univ.instantiate_univ_context (Univ.UInfoInd.univ_context mind.mind_universes)) in
+    let univs = 
+      Array.fold_left
+        (fun unvs pk ->
+           Univ.LSet.union
+             (univ_of_one_ind pk) unvs
+        )
+        Univ.LSet.empty mind.mind_packets 
+    in
+    let mindcnt =  Univ.UContext.constraints (Univ.instantiate_univ_context auctx) in
     let univs = Univ.LSet.union univs (Univ.universes_of_constraints mindcnt) in
     univs
-  end
-  else LSet.empty
+  in
+  match mind.mind_universes with
+  | Monomorphic_ind _ -> LSet.empty
+  | Polymorphic_ind auctx -> process auctx
+  | Cumulative_ind cumi -> process (Univ.ACumulativityInfo.univ_context cumi)
 
 let restrict_universe_context (univs,csts) s =
   (* Universes that are not necessary to typecheck the term.