Clean up universes of constants and inductives

16 files changed, 217 insertions, 112 deletions

diff --git a/checker/cic.mli b/checker/cic.mli
index f9d082ab1c..bbddb678bc 100644
--- a/checker/cic.mli
+++ b/checker/cic.mli
@@ -209,7 +209,9 @@ type constant_def =
   | Def of constr_substituted
   | OpaqueDef of lazy_constr
 
-type constant_universes = Univ.universe_context
+type constant_universes =
+  | Monomorphic_const of Univ.universe_context
+  | Polymorphic_const of Univ.abstract_universe_context
 
 (** The [typing_flags] are instructions to the type-checker which
     modify its behaviour. The typing flags used in the type-checking
@@ -226,7 +228,6 @@ type constant_body = {
     const_body : constant_def;
     const_type : constant_type;
     const_body_code : to_patch_substituted;
-    const_polymorphic : bool; (** Is it polymorphic or not *)
     const_universes : constant_universes;
     const_proj : projection_body option;
     const_inline_code : bool;
@@ -303,6 +304,11 @@ type one_inductive_body = {
     mind_reloc_tbl : reloc_table;
   }
 
+type abstrac_inductive_universes =
+  | Monomorphic_ind of Univ.universe_context
+  | Polymorphic_ind of Univ.abstract_universe_context
+  | Cumulative_ind of Univ.abstract_cumulativity_info
+
 type mutual_inductive_body = {
 
     mind_packets : one_inductive_body array;  (** The component of the mutual inductive block *)
@@ -321,11 +327,7 @@ type mutual_inductive_body = {
 
     mind_params_ctxt : rel_context;  (** The context of parameters (includes let-in declaration) *)
 
-    mind_polymorphic : bool; (** Is it polymorphic or not *)
-
-    mind_cumulative : bool; (** Is it cumulative or not *)
-
-    mind_universes : Univ.universe_info_ind; (** Local universe variables and constraints together with subtyping constraints *)
+    mind_universes : abstrac_inductive_universes; (** 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/checker/declarations.ml b/checker/declarations.ml
index ad93146d55..2eefe47816 100644
--- a/checker/declarations.ml
+++ b/checker/declarations.ml
@@ -521,6 +521,11 @@ let subst_template_cst_arity sub (ctx,s as arity) =
 
 let subst_arity sub s = subst_decl_arity subst_mps subst_template_cst_arity sub s
 
+let constant_is_polymorphic cb =
+  match cb.const_universes with
+  | Monomorphic_const _ -> false
+  | Polymorphic_const _ -> true
+
 (* TODO: should be changed to non-coping after Term.subst_mps *)
 (* NB: we leave bytecode and native code fields untouched *)
 let subst_const_body sub cb =
diff --git a/checker/declarations.mli b/checker/declarations.mli
index 456df83699..6fc71bb942 100644
--- a/checker/declarations.mli
+++ b/checker/declarations.mli
@@ -14,6 +14,7 @@ val body_of_constant : constant_body -> constr option
 val constant_has_body : constant_body -> bool
 val is_opaque : constant_body -> bool
 val opaque_univ_context : constant_body -> Univ.ContextSet.t
+val constant_is_polymorphic : constant_body -> bool
 
 (* Mutual inductives *)
 
diff --git a/checker/environ.ml b/checker/environ.ml
index 22d1eec178..11b8ea67cc 100644
--- a/checker/environ.ml
+++ b/checker/environ.ml
@@ -115,13 +115,15 @@ let add_constant kn cs env =
 	env_constants = new_constants } in
   { env with env_globals = new_globals }
 
-type const_evaluation_result = NoBody | Opaque
+type const_evaluation_result = NoBody | Opaque | IsProj
 
 (* Constant types *)
 
 let constraints_of cb u =
-  let univs = cb.const_universes in
-    Univ.subst_instance_constraints u (Univ.UContext.constraints univs)
+  match cb.const_universes with
+  | Monomorphic_const _ -> Univ.Constraint.empty
+  | Polymorphic_const ctx -> 
+    Univ.UContext.constraints (Univ.subst_instance_context u ctx)
 
 let map_regular_arity f = function
   | RegularArity a as ar -> 
@@ -132,23 +134,28 @@ let map_regular_arity f = function
 (* constant_type gives the type of a constant *)
 let constant_type env (kn,u) =
   let cb = lookup_constant kn env in
-    if cb.const_polymorphic then
-      let csts = constraints_of cb u in
-	(map_regular_arity (subst_instance_constr u) cb.const_type, csts)
-    else cb.const_type, Univ.Constraint.empty
+  match cb.const_universes with
+  | Monomorphic_const _ -> cb.const_type, Univ.Constraint.empty
+  | Polymorphic_const ctx -> 
+    let csts = constraints_of cb u in
+    (map_regular_arity (subst_instance_constr u) cb.const_type, csts)
 
 exception NotEvaluableConst of const_evaluation_result
 
 let constant_value env (kn,u) =
   let cb = lookup_constant kn env in
+  if cb.const_proj = None then
     match cb.const_body with
     | Def l_body -> 
       let b = force_constr l_body in
-	if cb.const_polymorphic then
-	  subst_instance_constr u (force_constr l_body)
-	else b
+      begin
+        match cb.const_universes with
+        | Monomorphic_const _ -> b
+        | Polymorphic_const _ -> subst_instance_constr u (force_constr l_body)
+      end
     | OpaqueDef _ -> raise (NotEvaluableConst Opaque)
     | Undef _ -> raise (NotEvaluableConst NoBody)
+  else raise (NotEvaluableConst IsProj)
 
 (* A global const is evaluable if it is defined and not opaque *)
 let evaluable_constant cst env =
diff --git a/checker/environ.mli b/checker/environ.mli
index 87f143d1bb..754c295d27 100644
--- a/checker/environ.mli
+++ b/checker/environ.mli
@@ -47,7 +47,7 @@ val check_constraints : Univ.constraints -> env -> bool
 val lookup_constant : constant -> env -> Cic.constant_body
 val add_constant : constant -> Cic.constant_body -> env -> env
 val constant_type : env -> constant puniverses -> constant_type Univ.constrained
-type const_evaluation_result = NoBody | Opaque
+type const_evaluation_result = NoBody | Opaque | IsProj
 exception NotEvaluableConst of const_evaluation_result
 val constant_value : env -> constant puniverses -> constr
 val evaluable_constant : constant -> env -> bool
diff --git a/checker/indtypes.ml b/checker/indtypes.ml
index cc3493aa25..54dec56b54 100644
--- a/checker/indtypes.ml
+++ b/checker/indtypes.ml
@@ -548,16 +548,20 @@ let check_subtyping_arity_constructor env (subst : constr -> constr) (arcn : con
 
 (* Check that the subtyping information inferred for inductive types in the block is correct. *)
 (* This check produces a value of the unit type if successful or raises an anomaly if check fails. *)
-let check_subtyping mib paramsctxt env_ar inds =
+let check_subtyping cumi paramsctxt env_ar inds =
   let numparams = rel_context_nhyps paramsctxt in
-  let sbsubst = Univ.UInfoInd.subtyping_susbst mib.mind_universes in
-  let other_instnace = Univ.UInfoInd.subtyping_other_instance mib.mind_universes in
+  let sbsubst = Univ.CumulativityInfo.subtyping_susbst cumi in
+  let other_instnace = Univ.CumulativityInfo.subtyping_other_instance cumi in
   let dosubst = subst_univs_level_constr sbsubst in
-  let uctx = Univ.UInfoInd.univ_context mib.mind_universes in
+  let uctx = Univ.CumulativityInfo.univ_context cumi in
   let uctx_other = Univ.UContext.make (other_instnace, Univ.UContext.constraints uctx) in
-  let env = Environ.push_context (Univ.instantiate_univ_context uctx) env_ar in
-  let env = Environ.push_context (Univ.instantiate_univ_context uctx_other) env in
-  let env = Environ.push_context (Univ.instantiate_univ_context (Univ.UInfoInd.subtyp_context mib.mind_universes)) env in
+  let env = Environ.push_context uctx env_ar 
+  in
+  let env = Environ.push_context uctx_other env 
+  in
+  let env =  Environ.push_context 
+      (Univ.CumulativityInfo.subtyp_context cumi) env
+  in
   (* process individual inductive types: *)
   Array.iter (fun { mind_user_lc = lc; mind_arity = arity } ->
       match arity with
@@ -573,7 +577,14 @@ let check_subtyping mib paramsctxt env_ar inds =
 let check_inductive env kn mib =
   Flags.if_verbose Feedback.msg_notice (str "  checking ind: " ++ MutInd.print kn);
   (* check mind_constraints: should be consistent with env *)
-  let env = Environ.push_context (Univ.instantiate_univ_context (Univ.UInfoInd.univ_context mib.mind_universes)) env in
+  let ind_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 env = Environ.push_context ind_ctx env in
   (* check mind_record : TODO ? check #constructor = 1 ? *)
   (* check mind_finite : always OK *)
   (* check mind_ntypes *)
@@ -591,8 +602,13 @@ let check_inductive env kn mib =
   (*  - check constructor types *)
   Array.iter (typecheck_one_inductive env_ar params mib) mib.mind_packets;
   (* check the inferred subtyping relation *)
-  if mib.mind_cumulative then
-    check_subtyping mib params env_ar mib.mind_packets;
+  let () = 
+    match mib.mind_universes with
+    | Monomorphic_ind _ | Polymorphic_ind _ -> ()
+    | Cumulative_ind acumi ->
+      check_subtyping 
+        (Univ.instantiate_cumulativity_info acumi) params env_ar mib.mind_packets
+  in
   (* check mind_nparams_rec: positivity condition *)
   check_positivity env_ar kn params mib.mind_nparams_rec mib.mind_packets;
   (* check mind_equiv... *)
diff --git a/checker/inductive.ml b/checker/inductive.ml
index 30c5f878a1..e1860a23f0 100644
--- a/checker/inductive.ml
+++ b/checker/inductive.ml
@@ -54,10 +54,31 @@ let inductive_params (mib,_) = mib.mind_nparams
 
 (** Polymorphic inductives *)
 
-let inductive_instance mib =
-  if mib.mind_polymorphic then
-    UContext.instance (UInfoInd.univ_context mib.mind_universes)
-  else Instance.empty
+let inductive_is_polymorphic mib =
+  match mib.mind_universes with
+  | Monomorphic_ind _ -> false
+  | Polymorphic_ind ctx -> true
+  | Cumulative_ind cumi -> true
+
+let inductive_is_cumulative mib =
+  match mib.mind_universes with
+  | Monomorphic_ind _ -> false
+  | Polymorphic_ind ctx -> false
+  | Cumulative_ind cumi -> true
+
+let inductive_polymorphic_instance mib =
+  match mib.mind_universes with
+  | Monomorphic_ind _ -> Univ.Instance.empty
+  | Polymorphic_ind ctx -> Univ.AUContext.instance ctx
+  | Cumulative_ind cumi -> 
+    Univ.AUContext.instance (Univ.ACumulativityInfo.univ_context cumi)
+
+let inductive_polymorphic_context mib =
+  match mib.mind_universes with
+  | Monomorphic_ind _ -> Univ.UContext.empty
+  | Polymorphic_ind ctx -> Univ.instantiate_univ_context ctx
+  | Cumulative_ind cumi -> 
+    Univ.instantiate_univ_context (Univ.ACumulativityInfo.univ_context cumi)
 
 (************************************************************************)
 
@@ -93,7 +114,7 @@ let instantiate_params full t u args sign =
 
 let full_inductive_instantiate mib u params sign =
   let dummy = Prop Null in
-  let t = mkArity (subst_instance_context u sign,dummy) in
+  let t = mkArity (Term.subst_instance_context u sign,dummy) in
     fst (destArity (instantiate_params true t u params mib.mind_params_ctxt))
 
 let full_constructor_instantiate ((mind,_),u,(mib,_),params) t =
@@ -199,7 +220,7 @@ let instantiate_universes env ctx ar argsorts =
 let type_of_inductive_gen env ((mib,mip),u) paramtyps =
   match mip.mind_arity with
   | RegularArity a ->
-    if not mib.mind_polymorphic then a.mind_user_arity
+    if not (inductive_is_polymorphic mib) then a.mind_user_arity
     else subst_instance_constr u a.mind_user_arity
   | TemplateArity ar ->
     let ctx = List.rev mip.mind_arity_ctxt in
diff --git a/checker/inductive.mli b/checker/inductive.mli
index ed3a7b53ce..9a5541f39b 100644
--- a/checker/inductive.mli
+++ b/checker/inductive.mli
@@ -22,7 +22,13 @@ type mind_specif = mutual_inductive_body * one_inductive_body
     Raises [Not_found] if the inductive type is not found. *)
 val lookup_mind_specif : env -> inductive -> mind_specif
 
-val inductive_instance : mutual_inductive_body -> Univ.universe_instance
+val inductive_is_polymorphic : mutual_inductive_body -> bool
+
+val inductive_is_cumulative : mutual_inductive_body -> bool
+
+val inductive_polymorphic_instance : mutual_inductive_body -> Univ.universe_instance
+
+val inductive_polymorphic_context : mutual_inductive_body -> Univ.universe_context
 
 val type_of_inductive : env -> mind_specif puniverses -> constr
 
diff --git a/checker/mod_checking.ml b/checker/mod_checking.ml
index 7f93e15609..15e9ae2951 100644
--- a/checker/mod_checking.ml
+++ b/checker/mod_checking.ml
@@ -1,4 +1,3 @@
-
 open Pp
 open Util
 open Names
@@ -26,21 +25,23 @@ let refresh_arity ar =
     | _ -> ar, Univ.ContextSet.empty
 
 let check_constant_declaration env kn cb =
-  Flags.if_verbose Feedback.msg_notice (str "  checking cst: " ++ prcon kn);
-  let env' =
-    if cb.const_polymorphic then
-      let inst = Univ.make_abstract_instance cb.const_universes in
-      let ctx = Univ.UContext.make (inst, Univ.UContext.constraints cb.const_universes) in
-        push_context ~strict:false ctx env
-    else push_context ~strict:true cb.const_universes env
+  Feedback.msg_notice (str "  checking cst:" ++ prcon kn);
+  let env', u =
+    match cb.const_universes with
+    | Monomorphic_const ctx -> push_context ~strict:true ctx env, Univ.Instance.empty
+    | Polymorphic_const auctx ->
+      let ctx = Univ.instantiate_univ_context auctx in
+      push_context ~strict:false ctx env, Univ.UContext.instance ctx
   in
   let envty, ty = 
     match cb.const_type with
       RegularArity ty ->
+        let ty = subst_instance_constr u ty in
         let ty', cu = refresh_arity ty in
         let envty = push_context_set cu env' in
         let _ = infer_type envty ty' in envty, ty
     | TemplateArity(ctxt,par) ->
+        assert(Univ.Instance.is_empty u);
         let _ = check_ctxt env' ctxt in
         check_polymorphic_arity env' ctxt par;
 	env', it_mkProd_or_LetIn (Sort(Type par.template_level)) ctxt 
@@ -48,6 +49,7 @@ let check_constant_declaration env kn cb =
   let () = 
     match body_of_constant cb with
     | Some bd ->
+      let bd = subst_instance_constr u bd in
       (match cb.const_proj with 
       | None -> let j = infer envty bd in
 		  conv_leq envty j ty
@@ -57,7 +59,7 @@ let check_constant_declaration env kn cb =
 	  conv_leq envty j ty)
     | None -> ()
   in
-  if cb.const_polymorphic then add_constant kn cb env
+  if constant_is_polymorphic cb then add_constant kn cb env
   else add_constant kn cb env'
 
 (** {6 Checking modules } *)
diff --git a/checker/modops.ml b/checker/modops.ml
index bed31143bf..be35c7e981 100644
--- a/checker/modops.ml
+++ b/checker/modops.ml
@@ -83,10 +83,10 @@ let strengthen_const mp_from l cb resolver =
     | Def _ -> cb
     | _ ->
       let con = Constant.make2 mp_from l in
-      let u = 
-	if cb.const_polymorphic then
-	  Univ.make_abstract_instance cb.const_universes
-	else Univ.Instance.empty
+      let u =
+        match cb.const_universes with
+      | Monomorphic_const _ -> Univ.Instance.empty
+      | Polymorphic_const auctx -> Univ.make_abstract_instance auctx
       in
       { cb with
 	const_body = Def (Declarations.from_val (Const (con,u))) }
diff --git a/checker/reduction.ml b/checker/reduction.ml
index 70c0bdad02..5010920bcb 100644
--- a/checker/reduction.ml
+++ b/checker/reduction.ml
@@ -156,22 +156,27 @@ let compare_stacks f fmind lft1 stk1 lft2 stk2 =
     cmp_rec (pure_stack lft1 stk1) (pure_stack lft2 stk2)
   else raise NotConvertible
 
-let convert_inductive_instances cv_pb uinfind u u' univs =
-  let ind_instance = Univ.UContext.instance (Univ.UInfoInd.univ_context uinfind) in
-  let ind_sbcst = Univ.UContext.constraints (Univ.UInfoInd.subtyp_context uinfind) in
+let convert_inductive_instances cv_pb cumi u u' univs =
+  let ind_instance =
+      Univ.AUContext.instance (Univ.ACumulativityInfo.univ_context cumi) in
+  let ind_subtypctx =  Univ.ACumulativityInfo.subtyp_context cumi in
   if not ((Univ.Instance.length ind_instance = Univ.Instance.length u) &&
           (Univ.Instance.length ind_instance = Univ.Instance.length u')) then
-     anomaly (Pp.str "Invalid inductive subtyping encountered!")
+    anomaly (Pp.str "Invalid inductive subtyping encountered!")
   else
     let comp_cst =
       let comp_subst = (Univ.Instance.append u u') in
-      Univ.subst_instance_constraints comp_subst ind_sbcst
+      Univ.UContext.constraints
+      (Univ.subst_instance_context comp_subst ind_subtypctx)
     in
     let comp_cst =
       match cv_pb with
         CONV ->
-        let comp_subst = (Univ.Instance.append u' u) in
-        let comp_cst' = (Univ.subst_instance_constraints comp_subst ind_sbcst) in
+        let comp_cst' =
+          let comp_subst = (Univ.Instance.append u' u) in
+          Univ.UContext.constraints
+            (Univ.subst_instance_context comp_subst ind_subtypctx)
+        in
         Univ.Constraint.union comp_cst comp_cst'
       | CUMUL -> comp_cst
     in
@@ -179,28 +184,32 @@ let convert_inductive_instances cv_pb uinfind u u' univs =
 
 let convert_inductives
     cv_pb (mind, ind) u1 sv1 u2 sv2 univs =
-  let num_param_arity =
-    mind.mind_nparams + mind.mind_packets.(ind).mind_nrealargs
-  in
-  if not (num_param_arity = sv1 && num_param_arity = sv2) then
-    convert_universes univs u1 u2
-  else
-    let uinfind = mind.mind_universes in
-    convert_inductive_instances cv_pb uinfind u1 u2 univs
+  match mind.mind_universes with
+  | Monomorphic_ind _ | Polymorphic_ind _ -> convert_universes univs u1 u2
+  | Cumulative_ind cumi ->
+    let num_param_arity =
+      mind.mind_nparams + mind.mind_packets.(ind).mind_nrealargs
+    in
+    if not (num_param_arity = sv1 && num_param_arity = sv2) then
+      convert_universes univs u1 u2
+    else
+      convert_inductive_instances cv_pb cumi u1 u2 univs
 
 let convert_constructors
     (mind, ind, cns) u1 sv1 u2 sv2 univs =
-  let num_cnstr_args =
-    let nparamsctxt =
-      mind.mind_nparams + mind.mind_packets.(ind).mind_nrealargs
+  match mind.mind_universes with
+  | Monomorphic_ind _ | Polymorphic_ind _ -> convert_universes univs u1 u2
+  | Cumulative_ind cumi ->
+    let num_cnstr_args =
+      let nparamsctxt =
+        mind.mind_nparams + mind.mind_packets.(ind).mind_nrealargs
+      in
+      nparamsctxt + mind.mind_packets.(ind).mind_consnrealargs.(cns - 1)
     in
-    nparamsctxt + mind.mind_packets.(ind).mind_consnrealargs.(cns - 1)
-  in
-  if not (num_cnstr_args = sv1 && num_cnstr_args = sv2) then
-    convert_universes univs u1 u2
-  else
-    let uinfind = mind.mind_universes in
-    convert_inductive_instances CONV uinfind u1 u2 univs
+    if not (num_cnstr_args = sv1 && num_cnstr_args = sv2) then
+      convert_universes univs u1 u2
+    else
+      convert_inductive_instances CONV cumi u1 u2 univs
 
 (* Convertibility of sorts *)
 
@@ -424,11 +433,8 @@ and eqappr univ cv_pb infos (lft1,st1) (lft2,st2) =
       if mind_equiv_infos infos ind1 ind2 then
         let mind = Environ.lookup_mind (fst ind1) (infos_env infos) in
         let () =
-          if mind.mind_polymorphic && mind.mind_cumulative then
-              convert_inductives cv_pb (mind, snd ind1) u1 (stack_args_size v1)
-                u2 (stack_args_size v2) univ
-          else
-            convert_universes univ u1 u2
+          convert_inductives cv_pb (mind, snd ind1) u1 (stack_args_size v1)
+            u2 (stack_args_size v2) univ
         in
         convert_stacks univ infos lft1 lft2 v1 v2
       else raise NotConvertible
@@ -437,12 +443,9 @@ and eqappr univ cv_pb infos (lft1,st1) (lft2,st2) =
       if Int.equal j1 j2 && mind_equiv_infos infos ind1 ind2 then
         let mind = Environ.lookup_mind (fst ind1) (infos_env infos) in
         let () =
-          if mind.mind_polymorphic && mind.mind_cumulative then
-            convert_constructors
-              (mind, snd ind1, j1) u1 (stack_args_size v1)
-              u2 (stack_args_size v2) univ
-          else
-            convert_universes univ u1 u2
+          convert_constructors
+            (mind, snd ind1, j1) u1 (stack_args_size v1)
+            u2 (stack_args_size v2) univ
         in
         convert_stacks univ infos lft1 lft2 v1 v2
       else raise NotConvertible
diff --git a/checker/subtyping.ml b/checker/subtyping.ml
index 8c10bd6eca..bfe19584a7 100644
--- a/checker/subtyping.ml
+++ b/checker/subtyping.ml
@@ -88,18 +88,25 @@ let check_inductive  env mp1 l info1 mib2 spec2 subst1 subst2=
   let check_conv f = check_conv_error error f in
   let mib1 =
     match info1 with
-      | IndType ((_,0), mib) -> mib
+      | IndType ((_,0), mib) -> subst_mind subst1 mib
       | _ -> error ()
   in
   let mib2 = subst_mind subst2 mib2 in
   let check eq f = if not (eq (f mib1) (f mib2)) then error () in
-  let bool_equal (x : bool) (y : bool) = x = y in
-  let u = 
-    check bool_equal (fun x -> x.mind_polymorphic);
-    if mib1.mind_polymorphic then (
-      check Univ.Instance.equal (fun x -> Univ.UContext.instance (Univ.UInfoInd.univ_context x.mind_universes));
-      Univ.UContext.instance (Univ.UInfoInd.univ_context mib1.mind_universes))
-    else Univ.Instance.empty
+  let u =
+    let process inst inst' =
+      if Univ.Instance.equal inst inst' then inst else error ()
+    in
+    match mib1.mind_universes, mib2.mind_universes with
+    | Monomorphic_ind _, Monomorphic_ind _ -> Univ.Instance.empty
+    | Polymorphic_ind auctx, Polymorphic_ind auctx' ->
+      process
+        (Univ.AUContext.instance auctx) (Univ.AUContext.instance auctx')
+    | Cumulative_ind cumi, Cumulative_ind cumi' ->
+      process
+        (Univ.AUContext.instance (Univ.ACumulativityInfo.univ_context cumi))
+        (Univ.AUContext.instance (Univ.ACumulativityInfo.univ_context cumi'))
+    | _ -> error ()
   in
   let eq_projection_body p1 p2 =
     let check eq f = if not (eq (f p1) (f p2)) then error () in
@@ -308,7 +315,7 @@ let check_constant env mp1 l info1 cb2 spec2 subst1 subst2 =
 		      "inductive type and give a definition to map the old name to the new " ^
 		      "name.")));
       if constant_has_body cb2 then error () ;
-      let u = inductive_instance mind1 in
+      let u = inductive_polymorphic_instance mind1 in
       let arity1 = type_of_inductive env ((mind1,mind1.mind_packets.(i)),u) in
       let typ2 = Typeops.type_of_constant_type env cb2.const_type in
        check_conv conv_leq env arity1 typ2
@@ -319,7 +326,7 @@ let check_constant env mp1 l info1 cb2 spec2 subst1 subst2 =
        "constructor and give a definition to map the old name to the new " ^
        "name.")));
       if constant_has_body cb2 then error () ;
-      let u1 = inductive_instance mind1 in
+      let u1 = inductive_polymorphic_instance mind1 in
       let ty1 = type_of_constructor (cstr,u1) (mind1,mind1.mind_packets.(i)) in
       let ty2 = Typeops.type_of_constant_type env cb2.const_type in
        check_conv conv env ty1 ty2
diff --git a/checker/typeops.ml b/checker/typeops.ml
index 0163db3347..543f9acced 100644
--- a/checker/typeops.ml
+++ b/checker/typeops.ml
@@ -329,7 +329,6 @@ let rec execute env cstr =
         let pj = execute env p in
         let lfj = execute_array env lf in
         judge_of_case env ci (p,pj) (c,cj) lfj
-
     | Fix ((_,i as vni),recdef) ->
         let fix_ty = execute_recdef env recdef i in
         let fix = (vni,recdef) in
diff --git a/checker/univ.ml b/checker/univ.ml
index 92b6a9e867..0ee4686c1a 100644
--- a/checker/univ.ml
+++ b/checker/univ.ml
@@ -1184,7 +1184,11 @@ end
 
 type universe_context = UContext.t
 
-module UInfoInd =
+module AUContext = UContext
+
+type abstract_universe_context = AUContext.t
+
+module CumulativityInfo =
 struct
   type t = universe_context * universe_context
 
@@ -1223,7 +1227,10 @@ struct
 
 end
 
-type universe_info_ind = UInfoInd.t
+type cumulativity_info = CumulativityInfo.t
+
+module ACumulativityInfo = CumulativityInfo
+type abstract_cumulativity_info = ACumulativityInfo.t
 
 module ContextSet =
 struct
@@ -1281,7 +1288,10 @@ let subst_instance_constraint s (u,d,v as c) =
 let subst_instance_constraints s csts =
   Constraint.fold 
     (fun c csts -> Constraint.add (subst_instance_constraint s c) csts)
-    csts Constraint.empty 
+    csts Constraint.empty
+
+let subst_instance_context inst (inner_inst, inner_constr) =
+  (inner_inst, subst_instance_constraints inst inner_constr)
 
 let make_abstract_instance (ctx, _) = 
   Array.mapi (fun i l -> Level.var i) ctx
@@ -1290,8 +1300,8 @@ let make_abstract_instance (ctx, _) =
 let instantiate_univ_context (ctx, csts) = 
   (ctx, subst_instance_constraints ctx csts)
 
-let instantiate_univ_constraints u (_, csts) = 
-  subst_instance_constraints u csts
+let instantiate_cumulativity_info (ctx, ctx') = 
+  (instantiate_univ_context ctx, instantiate_univ_context ctx')
 
 (** With level to universe substitutions. *)
 type universe_subst_fn = universe_level -> universe
diff --git a/checker/univ.mli b/checker/univ.mli
index 018f8aee2e..a503924708 100644
--- a/checker/univ.mli
+++ b/checker/univ.mli
@@ -204,7 +204,17 @@ end
 
 type universe_context = UContext.t
 
-module UInfoInd :
+module AUContext :
+sig
+  type t
+
+  val instance : t -> Instance.t
+
+end
+
+type abstract_universe_context = AUContext.t
+
+module CumulativityInfo :
 sig
   type t
 
@@ -223,7 +233,18 @@ sig
 
 end
 
-type universe_info_ind = UInfoInd.t
+type cumulativity_info = CumulativityInfo.t
+
+module ACumulativityInfo :
+sig
+  type t
+
+  val univ_context : t -> abstract_universe_context
+  val subtyp_context : t -> abstract_universe_context
+
+end
+
+type abstract_cumulativity_info = ACumulativityInfo.t
 
 module ContextSet :
   sig 
@@ -255,17 +276,17 @@ val subst_univs_universe : universe_subst_fn -> universe -> universe
 (** Substitution of instances *)
 val subst_instance_instance : universe_instance -> universe_instance -> universe_instance
 val subst_instance_universe : universe_instance -> universe -> universe
-val subst_instance_constraints : universe_instance -> constraints -> constraints
+val subst_instance_context : universe_instance -> abstract_universe_context -> universe_context
 
 (* val make_instance_subst : universe_instance -> universe_level_subst *)
 (* val make_inverse_instance_subst : universe_instance -> universe_level_subst *)
 
 (** Get the instantiated graph. *)
-val instantiate_univ_context : universe_context -> universe_context
-val instantiate_univ_constraints : universe_instance -> universe_context -> constraints
+val instantiate_univ_context : abstract_universe_context -> universe_context
+val instantiate_cumulativity_info : abstract_cumulativity_info -> cumulativity_info
 
 (** Build the relative instance corresponding to the context *)
-val make_abstract_instance : universe_context -> universe_instance
+val make_abstract_instance : abstract_universe_context -> universe_instance
 									    
 (** {6 Pretty-printing of universes. } *)
 
diff --git a/checker/values.ml b/checker/values.ml
index c58f56a9bd..422729ed55 100644
--- a/checker/values.ml
+++ b/checker/values.ml
@@ -13,7 +13,7 @@
 To ensure this file is up-to-date, 'make' now compares the md5 of cic.mli
 with a copy we maintain here:
 
-MD5 6153d4f8fb414a8f14797636ab10f55e  checker/cic.mli
+MD5 6950230ca9e99e9cc3a70488d8ab824c  checker/cic.mli
 
 *)
 
@@ -109,6 +109,8 @@ let v_cstrs =
 
 let v_instance = Annot ("instance", Array v_level)
 let v_context = v_tuple "universe_context" [|v_instance;v_cstrs|]
+let v_abs_context = v_context (* only for clarity *)
+let v_abs_cum_info = v_tuple "cumulativity_info" [|v_abs_context; v_context|]
 let v_context_set = v_tuple "universe_context_set" [|v_hset v_level;v_cstrs|]
 
 (** kernel/term *)
@@ -215,13 +217,14 @@ let v_projbody =
 let v_typing_flags =
   v_tuple "typing_flags" [|v_bool; v_bool|]
 
+let v_const_univs = v_sum "constant_universes" 0 [|[|v_context|]; [|v_abs_context|]|]
+
 let v_cb = v_tuple "constant_body"
   [|v_section_ctxt;
     v_cst_def;
     v_cst_type;
     Any;
-    v_bool;
-    v_context;
+    v_const_univs;
     Opt v_projbody;
     v_bool;
     v_typing_flags|]
@@ -262,6 +265,10 @@ let v_finite = v_enum "recursivity_kind" 3
 let v_mind_record = Annot ("mind_record", 
 			   Opt (Opt (v_tuple "record" [| v_id; Array v_cst; Array v_projbody |])))
 
+let v_ind_pack_univs = 
+  v_sum "abstract_inductive_universes" 0
+    [|[|v_context|]; [|v_abs_context|]; [|v_abs_cum_info|]|]
+
 let v_ind_pack = v_tuple "mutual_inductive_body"
   [|Array v_one_ind;
     v_mind_record;
@@ -271,9 +278,7 @@ let v_ind_pack = v_tuple "mutual_inductive_body"
     Int;
     Int;
     v_rctxt;
-    v_bool;
-    v_bool;
-    v_tuple "universes" [|v_context; v_context|];
+    v_ind_pack_univs; (* universes *)
     Opt v_bool;
     v_typing_flags|]