Clean up universes of constants and inductives

78 files changed, 1187 insertions, 714 deletions

diff --git a/API/API.mli b/API/API.mli
index a993b0277..ecce22c1d 100644
--- a/API/API.mli
+++ b/API/API.mli
@@ -84,9 +84,11 @@ sig
   end
 
   type universe_context = UContext.t
-  [@@ocaml.deprecated "alias of API.Names.UContext.t"]
+  [@@ocaml.deprecated "alias of API.Univ.UContext.t"]
 
-  type universe_info_ind = Univ.UInfoInd.t
+  type abstract_universe_context = Univ.AUContext.t
+  type cumulativity_info = Univ.CumulativityInfo.t
+  type abstract_cumulativity_info = Univ.ACumulativityInfo.t
 
   module LSet : module type of struct include Univ.LSet end
   module ContextSet : 
@@ -1047,12 +1049,12 @@ sig
         proj_body : Term.constr;
       }
   type typing_flags = Declarations.typing_flags
+
   type constant_body = Declarations.constant_body = {
         const_hyps : Context.Named.t;
         const_body : constant_def;
         const_type : constant_type;
         const_body_code : Cemitcodes.to_patch_substituted option;
-        const_polymorphic : bool;
         const_universes : constant_universes;
         const_proj : projection_body option;
         const_inline_code : bool;
@@ -1085,6 +1087,13 @@ sig
                        | MEident of Names.ModPath.t
                        | MEapply of module_alg_expr * Names.ModPath.t
                        | MEwith of module_alg_expr * with_declaration
+
+  type abstrac_inductive_universes = Declarations.abstrac_inductive_universes =
+    | Monomorphic_ind of Univ.UContext.t
+    | Polymorphic_ind of Univ.abstract_universe_context
+    | Cumulative_ind of Univ.abstract_cumulativity_info
+
+
   type mutual_inductive_body = Declarations.mutual_inductive_body = {
         mind_packets : one_inductive_body array;
         mind_record : Declarations.record_body option;
@@ -1094,9 +1103,7 @@ sig
         mind_nparams : int;
         mind_nparams_rec : int;
         mind_params_ctxt : Context.Rel.t;
-        mind_polymorphic : bool;
-        mind_cumulative : bool;
-        mind_universes : Univ.universe_info_ind;
+        mind_universes : abstrac_inductive_universes;
         mind_private : bool option;
         mind_typing_flags : Declarations.typing_flags;
       }
diff --git a/checker/cic.mli b/checker/cic.mli
index f9d082ab1..bbddb678b 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 ad93146d5..2eefe4781 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 456df8369..6fc71bb94 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 22d1eec17..11b8ea67c 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 87f143d1b..754c295d2 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 cc3493aa2..54dec56b5 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 30c5f878a..e1860a23f 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 ed3a7b53c..9a5541f39 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 7f93e1560..15e9ae295 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 bed31143b..be35c7e98 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 70c0bdad0..5010920bc 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 8c10bd6ec..bfe19584a 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 0163db334..543f9acce 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 92b6a9e86..0ee4686c1 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 018f8aee2..a50392470 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 c58f56a9b..422729ed5 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|]
 
diff --git a/dev/base_include b/dev/base_include
index f9af0696b..98cf67256 100644
--- a/dev/base_include
+++ b/dev/base_include
@@ -196,7 +196,7 @@ let qid = Libnames.qualid_of_string;;
 (* parsing of terms *)
 
 let parse_constr = Pcoq.parse_string Pcoq.Constr.constr;;
-let parse_tac    = Pcoq.parse_string Ltac_plugin.Pltac.tactic;;
+(*let parse_tac    = Pcoq.parse_string Ltac_plugin.Pltac.tactic;;*)
 let parse_vernac = Pcoq.parse_string Pcoq.Vernac_.vernac;;
 
 (* build a term of type glob_constr without type-checking or resolution of 
diff --git a/dev/include b/dev/include
index 4835b360d..1d87456de 100644
--- a/dev/include
+++ b/dev/include
@@ -41,7 +41,7 @@
 #install_printer  (* univ context *) ppuniverse_context;;
 #install_printer  (* univ context future *) ppuniverse_context_future;;
 #install_printer  (* univ context set *) ppuniverse_context_set;;
-#install_printer  (* univ info *) ppuniverse_info;;
+#install_printer  (* univ info *) ppcumulativity_info;;
 #install_printer  (* univ set *) ppuniverse_set;;
 #install_printer  (* univ instance *) ppuniverse_instance;;
 #install_printer  (* univ subst *) ppuniverse_subst;;
diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index e902da0b1..abf6db1b7 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -215,7 +215,7 @@ let ppuniverseconstraints c = pp (Universes.Constraints.pr c)
 let ppuniverse_context_future c = 
   let ctx = Future.force c in
     ppuniverse_context ctx
-let ppuniverse_info c = pp (Univ.pr_universe_info_ind Univ.Level.pr c)
+let ppcumulativity_info c = pp (Univ.pr_cumulativity_info Univ.Level.pr c)
 let ppuniverses u = pp (UGraph.pr_universes Level.pr u)
 let ppnamedcontextval e =
   pp (pr_named_context (Global.env ()) Evd.empty (named_context_of_val e))
diff --git a/engine/universes.ml b/engine/universes.ml
index a12b42ab1..bd4d75930 100644
--- a/engine/universes.ml
+++ b/engine/universes.ml
@@ -283,11 +283,11 @@ let new_Type_sort dp = Type (new_univ dp)
 
 let fresh_universe_instance ctx =
   Instance.subst_fn (fun _ -> new_univ_level (Global.current_dirpath ())) 
-    (UContext.instance ctx)
+    (AUContext.instance ctx)
 
 let fresh_instance_from_context ctx =
   let inst = fresh_universe_instance ctx in
-  let constraints = instantiate_univ_constraints inst ctx in
+  let constraints = UContext.constraints (subst_instance_context inst ctx) in
     inst, constraints
 
 let fresh_instance ctx =
@@ -296,13 +296,13 @@ let fresh_instance ctx =
     Instance.subst_fn (fun v -> 
       let u = new_univ_level (Global.current_dirpath ()) in
 	ctx' := LSet.add u !ctx'; u) 
-      (UContext.instance ctx)
+      (AUContext.instance ctx)
   in !ctx', inst
 
 let existing_instance ctx inst = 
   let () = 
     let a1 = Instance.to_array inst 
-    and a2 = Instance.to_array (UContext.instance ctx) in
+    and a2 = Instance.to_array (AUContext.instance ctx) in
     let len1 = Array.length a1 and len2 = Array.length a2 in 
       if not (len1 == len2) then
 	CErrors.user_err ~hdr:"Universes"
@@ -317,59 +317,75 @@ let fresh_instance_from ctx inst =
     | Some inst -> existing_instance ctx inst
     | None -> fresh_instance ctx 
   in
-  let constraints = instantiate_univ_constraints inst ctx in
+  let constraints = UContext.constraints (subst_instance_context inst ctx) in
     inst, (ctx', constraints)
 
 let unsafe_instance_from ctx =
-  (Univ.UContext.instance ctx, ctx)
+  (Univ.AUContext.instance ctx, Univ.instantiate_univ_context ctx)
     
 (** Fresh universe polymorphic construction *)
 
 let fresh_constant_instance env c inst =
   let cb = lookup_constant c env in
-    if cb.Declarations.const_polymorphic then
-      let inst, ctx =
-        fresh_instance_from
-          (Declareops.universes_of_constant (Environ.opaque_tables env) cb) inst
-      in
-	((c, inst), ctx)
-    else ((c,Instance.empty), ContextSet.empty)
+  match cb.Declarations.const_universes with
+  | Declarations.Monomorphic_const _ -> ((c,Instance.empty), ContextSet.empty)
+  | Declarations.Polymorphic_const auctx -> 
+    let inst, ctx =
+      fresh_instance_from auctx inst
+    in
+    ((c, inst), ctx)
 
 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 (Univ.UInfoInd.univ_context mib.Declarations.mind_universes) inst in
-	((ind,inst), ctx)
-    else ((ind,Instance.empty), ContextSet.empty)
+  match mib.Declarations.mind_universes with
+  | Declarations.Monomorphic_ind _ ->
+    ((ind,Instance.empty), ContextSet.empty)
+  | Declarations.Polymorphic_ind uactx ->
+    let inst, ctx = (fresh_instance_from uactx) inst in 
+     ((ind,inst), ctx)
+  | Declarations.Cumulative_ind acumi ->
+    let inst, ctx = 
+      fresh_instance_from (Univ.ACumulativityInfo.univ_context acumi) inst
+    in ((ind,inst), ctx)
 
 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 (Univ.UInfoInd.univ_context mib.Declarations.mind_universes) inst in
+  match mib.Declarations.mind_universes with
+  | Declarations.Monomorphic_ind _ -> (((ind,i),Instance.empty), ContextSet.empty)
+  | Declarations.Polymorphic_ind auctx ->
+    let inst, ctx = fresh_instance_from auctx  inst in
 	(((ind,i),inst), ctx)
-    else (((ind,i),Instance.empty), ContextSet.empty)
+  | Declarations.Cumulative_ind acumi ->
+    let inst, ctx = fresh_instance_from (ACumulativityInfo.univ_context acumi) inst in
+    (((ind,i),inst), ctx)
 
 let unsafe_constant_instance env c =
   let cb = lookup_constant c env in
-    if cb.Declarations.const_polymorphic then
-      let inst, ctx = unsafe_instance_from
-        (Declareops.universes_of_constant (Environ.opaque_tables env) cb) in
-	((c, inst), ctx)
-    else ((c,Instance.empty), UContext.empty)
+  match cb.Declarations.const_universes with
+  | Declarations.Monomorphic_const _ ->
+    ((c,Instance.empty), UContext.empty)
+  | Declarations.Polymorphic_const auctx ->
+    let inst, ctx = unsafe_instance_from auctx in ((c, inst), ctx)
 
 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 (Univ.UInfoInd.univ_context mib.Declarations.mind_universes) in
-	((ind,inst), ctx)
-    else ((ind,Instance.empty), UContext.empty)
+  match mib.Declarations.mind_universes with
+  | Declarations.Monomorphic_ind _ -> ((ind,Instance.empty), UContext.empty)
+  | Declarations.Polymorphic_ind auctx ->
+    let inst, ctx = unsafe_instance_from auctx in ((ind,inst), ctx)
+  | Declarations.Cumulative_ind acumi ->
+    let inst, ctx = unsafe_instance_from (ACumulativityInfo.univ_context acumi) in
+    ((ind,inst), ctx)
 
 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 (Univ.UInfoInd.univ_context mib.Declarations.mind_universes) in
-	(((ind,i),inst), ctx)
-    else (((ind,i),Instance.empty), UContext.empty)
+  match mib.Declarations.mind_universes with
+  | Declarations.Monomorphic_ind _ -> (((ind, i),Instance.empty), UContext.empty)
+  | Declarations.Polymorphic_ind auctx ->
+    let inst, ctx = unsafe_instance_from auctx in (((ind, i),inst), ctx)
+  | Declarations.Cumulative_ind acumi ->
+    let inst, ctx = unsafe_instance_from (ACumulativityInfo.univ_context acumi) in
+    (((ind, i),inst), ctx)
 
 open Globnames
 
@@ -452,26 +468,49 @@ let type_of_reference env r =
   | ConstRef c ->
      let cb = Environ.lookup_constant c env in
      let ty = Typeops.type_of_constant_type env cb.const_type in
-       if cb.const_polymorphic then
-	 let inst, ctx = fresh_instance_from (Declareops.universes_of_constant (Environ.opaque_tables env) cb) None in
-	   Vars.subst_instance_constr inst ty, ctx
-       else ty, ContextSet.empty
-
+     begin
+       match cb.const_universes with
+       | Monomorphic_const _ -> ty, ContextSet.empty
+       | Polymorphic_const auctx ->
+         let inst, ctx = fresh_instance_from auctx None in
+         Vars.subst_instance_constr inst ty, ctx
+     end
   | 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 (Univ.UInfoInd.univ_context mib.mind_universes) None in
+     begin
+       match mib.mind_universes with
+       | Monomorphic_ind _ ->
+         let ty = Inductive.type_of_inductive env (specif, Univ.Instance.empty) in
+	 ty, ContextSet.empty
+       | Polymorphic_ind auctx ->
+         let inst, ctx = fresh_instance_from auctx  None in
 	 let ty = Inductive.type_of_inductive env (specif, inst) in
-	   ty, ctx
-       else
-	 let ty = Inductive.type_of_inductive env (specif, Univ.Instance.empty) in
-	   ty, ContextSet.empty
+         ty, ctx
+       | Cumulative_ind cumi ->
+         let inst, ctx = 
+           fresh_instance_from (ACumulativityInfo.univ_context cumi) None
+         in
+         let ty = Inductive.type_of_inductive env (specif, inst) in
+         ty, ctx
+     end
+	 
   | 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 (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
+    let (mib,oib as specif) = 
+      Inductive.lookup_mind_specif env (inductive_of_constructor cstr) 
+    in
+    begin
+       match mib.mind_universes with
+       | Monomorphic_ind _ ->
+         Inductive.type_of_constructor (cstr,Instance.empty) specif, ContextSet.empty
+       | Polymorphic_ind auctx ->
+         let inst, ctx = fresh_instance_from auctx None in
+	 Inductive.type_of_constructor (cstr,inst) specif, ctx
+       | Cumulative_ind cumi ->
+         let inst, ctx = 
+           fresh_instance_from (ACumulativityInfo.univ_context cumi) None 
+         in
+	 Inductive.type_of_constructor (cstr,inst) specif, ctx
+     end
 
 let type_of_global t = type_of_reference (Global.env ()) t
 
@@ -1098,4 +1137,4 @@ let univ_inf_ind_from_universe_context univcst =
   let freshunivs = Instance.of_array
       (Array.map (fun _ -> new_univ_level ())
          (Instance.to_array (UContext.instance univcst)))
-  in UInfoInd.from_universe_context univcst freshunivs
+  in CumulativityInfo.from_universe_context univcst freshunivs
diff --git a/engine/universes.mli b/engine/universes.mli
index c600f4af6..5ce5e4a42 100644
--- a/engine/universes.mli
+++ b/engine/universes.mli
@@ -101,10 +101,10 @@ val eq_constr_universes_proj : env -> constr -> constr -> bool universe_constrai
 (** Build a fresh instance for a given context, its associated substitution and 
     the instantiated constraints. *)
 
-val fresh_instance_from_context : universe_context -> 
+val fresh_instance_from_context : abstract_universe_context -> 
   universe_instance constrained
 
-val fresh_instance_from : universe_context -> universe_instance option ->
+val fresh_instance_from : abstract_universe_context -> universe_instance option ->
   universe_instance in_universe_context_set
 
 val fresh_sort_in_family : env -> sorts_family -> 
@@ -228,4 +228,4 @@ val solve_constraints_system : universe option array -> universe array -> univer
 
 (** Given a universe context representing constraints of an inductive
     this function produces a UInfoInd.t that with the trivial subtyping relation. *)
-val univ_inf_ind_from_universe_context : universe_context -> universe_info_ind
+val univ_inf_ind_from_universe_context : universe_context -> cumulativity_info
diff --git a/kernel/cbytegen.ml b/kernel/cbytegen.ml
index 57b397e6f..02c6a2c71 100644
--- a/kernel/cbytegen.ml
+++ b/kernel/cbytegen.ml
@@ -992,8 +992,8 @@ let compile_constant_body fail_on_error env univs = function
       let body = Mod_subst.force_constr sb in
       let instance_size =
         match univs with
-        | None -> 0
-        | Some univ -> Univ.UContext.size univ
+        | Monomorphic_const _ -> 0
+        | Polymorphic_const univ -> Univ.AUContext.size univ
       in
       match kind_of_term body with
 	| Const (kn',u) when is_univ_copy instance_size u ->
diff --git a/kernel/cbytegen.mli b/kernel/cbytegen.mli
index c0f48641c..48c2e4533 100644
--- a/kernel/cbytegen.mli
+++ b/kernel/cbytegen.mli
@@ -10,7 +10,7 @@ val compile : bool -> (* Fail on error with a nice user message, otherwise simpl
 (** init, fun, fv *)
 
 val compile_constant_body : bool ->
-			    env -> constant_universes option -> constant_def -> body_code option
+			    env -> constant_universes -> constant_def -> body_code option
 
 (** Shortcut of the previous function used during module strengthening *)
 
diff --git a/kernel/cooking.ml b/kernel/cooking.ml
index 4deadff0a..000865364 100644
--- a/kernel/cooking.ml
+++ b/kernel/cooking.ml
@@ -153,8 +153,7 @@ type inline = bool
 
 type result =
   constant_def * constant_type * projection_body option * 
-    bool * constant_universes * inline
-    * Context.Named.t option
+    constant_universes * inline * Context.Named.t option
 
 let on_body ml hy f = function
   | Undef _ as x -> x
@@ -179,17 +178,21 @@ let cook_constr { Opaqueproof.modlist ; abstract } c =
   abstract_constant_body (expmod c) hyps
 
 let lift_univs cb subst =
-  if cb.const_polymorphic && not (Univ.LMap.is_empty subst) then
-    let inst = Univ.UContext.instance cb.const_universes in
-    let cstrs = Univ.UContext.constraints cb.const_universes in
-    let len = Univ.LMap.cardinal subst in
-    let subst = 
-      Array.fold_left_i (fun i acc v -> Univ.LMap.add (Level.var i) (Level.var (i + len)) acc)
-	subst (Univ.Instance.to_array inst)
-    in
-    let cstrs' = Univ.subst_univs_level_constraints subst cstrs in
-      subst, Univ.UContext.make (inst,cstrs')
-  else subst, cb.const_universes
+  match cb.const_universes with
+  | Monomorphic_const ctx -> subst, (Monomorphic_const ctx)
+  | Polymorphic_const auctx ->  
+    if (Univ.LMap.is_empty subst) then
+      subst, (Polymorphic_const auctx)
+    else
+      let inst = Univ.AUContext.instance auctx in
+      let len = Univ.LMap.cardinal subst in
+      let subst = 
+        Array.fold_left_i 
+          (fun i acc v -> Univ.LMap.add (Level.var i) (Level.var (i + len)) acc)
+	  subst (Univ.Instance.to_array inst)
+      in
+      let auctx' = Univ.subst_univs_level_abstract_universe_context subst auctx in
+      subst, (Polymorphic_const auctx')
 
 let cook_constant ~hcons env { from = cb; info } =
   let { Opaqueproof.modlist; abstract } = info in
@@ -243,15 +246,15 @@ let cook_constant ~hcons env { from = cb; info } =
 	proj_eta = etab, etat;
 	proj_type = ty'; proj_body = c' }
   in
-  let univs = 
-    let abs' = 
-      if cb.const_polymorphic then abs_ctx
-      else instantiate_univ_context abs_ctx
-    in
-      UContext.union abs' univs
+  let univs =
+    match univs with
+    | Monomorphic_const ctx -> 
+      Monomorphic_const (UContext.union (instantiate_univ_context abs_ctx) ctx)
+    | Polymorphic_const auctx -> 
+      Polymorphic_const (AUContext.union abs_ctx auctx)
   in
     (body, typ, Option.map projection cb.const_proj, 
-     cb.const_polymorphic, univs, cb.const_inline_code, 
+     univs, cb.const_inline_code, 
      Some const_hyps)
 
 (* let cook_constant_key = Profile.declare_profile "cook_constant" *)
diff --git a/kernel/cooking.mli b/kernel/cooking.mli
index 7d47eba23..9db85a4a1 100644
--- a/kernel/cooking.mli
+++ b/kernel/cooking.mli
@@ -18,8 +18,7 @@ type inline = bool
 
 type result =
   constant_def * constant_type * projection_body option * 
-    bool * constant_universes * inline
-    * Context.Named.t option
+    constant_universes * inline * Context.Named.t option
 
 val cook_constant : hcons:bool -> env -> recipe -> result
 val cook_constr : Opaqueproof.cooking_info -> Term.constr -> Term.constr
diff --git a/kernel/declarations.ml b/kernel/declarations.ml
index ae4732456..f3b7ae2b2 100644
--- a/kernel/declarations.ml
+++ b/kernel/declarations.ml
@@ -64,7 +64,9 @@ type constant_def =
   | Def of constr Mod_subst.substituted   (** or a transparent global definition *)
   | OpaqueDef of Opaqueproof.opaque       (** or an opaque global definition *)
 
-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
@@ -83,7 +85,6 @@ type constant_body = {
     const_body : constant_def;
     const_type : constant_type;
     const_body_code : Cemitcodes.to_patch_substituted option;
-    const_polymorphic : bool; (** Is it polymorphic or not *)
     const_universes : constant_universes;
     const_proj : projection_body option;
     const_inline_code : bool;
@@ -168,6 +169,11 @@ type one_inductive_body = {
     mind_reloc_tbl :  Cbytecodes.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 *)
@@ -186,11 +192,7 @@ type mutual_inductive_body = {
 
     mind_params_ctxt : Context.Rel.t;  (** 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; (** Information about monomorphic/polymorphic/cumulative inductives and their universes *)
 
     mind_private : bool option; (** allow pattern-matching: Some true ok, Some false blocked *)
 
diff --git a/kernel/declareops.ml b/kernel/declareops.ml
index 1d91b2d41..72b490768 100644
--- a/kernel/declareops.ml
+++ b/kernel/declareops.ml
@@ -45,14 +45,15 @@ let hcons_template_arity ar =
 (** {6 Constants } *)
 
 let instantiate cb c =
-  if cb.const_polymorphic then 
-    Vars.subst_instance_constr (Univ.UContext.instance cb.const_universes) c
-  else c
+  match cb.const_universes with
+  | Monomorphic_const _ -> c
+  | Polymorphic_const ctx -> 
+     Vars.subst_instance_constr (Univ.AUContext.instance ctx) c
 
-let instantiate_constraints cb cst =
-  if cb.const_polymorphic then 
-    Univ.subst_instance_constraints (Univ.UContext.instance cb.const_universes) cst
-  else cst
+let constant_is_polymorphic cb =
+  match cb.const_universes with
+  | Monomorphic_const _ -> false
+  | Polymorphic_const _ -> true
 
 let body_of_constant otab cb = match cb.const_body with
   | Undef _ -> None
@@ -67,34 +68,55 @@ let type_of_constant cb =
   | TemplateArity _ as x -> x
 
 let constraints_of_constant otab cb =
-  let cst = Univ.Constraint.union 
-    (Univ.UContext.constraints cb.const_universes)
-    (match cb.const_body with
-    | Undef _ -> Univ.empty_constraint
-    | Def c -> Univ.empty_constraint
-    | OpaqueDef o ->
-        Univ.ContextSet.constraints (Opaqueproof.force_constraints otab o))
-   in instantiate_constraints cb cst
+  match cb.const_universes with
+  | Polymorphic_const ctx -> 
+    Univ.UContext.constraints (Univ.instantiate_univ_context ctx)
+  | Monomorphic_const ctx -> 
+    Univ.Constraint.union 
+      (Univ.UContext.constraints ctx)
+      (match cb.const_body with
+       | Undef _ -> Univ.empty_constraint
+       | Def c -> Univ.empty_constraint
+       | OpaqueDef o ->
+         Univ.ContextSet.constraints (Opaqueproof.force_constraints otab o))
 
 let universes_of_constant otab cb = 
   match cb.const_body with
-  | Undef _ | Def _ -> cb.const_universes
+  | Undef _ | Def _ ->
+    begin
+      match cb.const_universes with
+      | Monomorphic_const ctx -> ctx
+      | Polymorphic_const ctx -> Univ.instantiate_univ_context ctx
+    end
   | OpaqueDef o -> 
-      let body_uctxs = Opaqueproof.force_constraints otab o in
-      assert(not cb.const_polymorphic || Univ.ContextSet.is_empty body_uctxs);
-      let uctxs = Univ.ContextSet.of_context cb.const_universes in
-      Univ.ContextSet.to_context (Univ.ContextSet.union body_uctxs uctxs) 
+    let body_uctxs = Opaqueproof.force_constraints otab o in
+    match cb.const_universes with
+    | Monomorphic_const ctx ->
+      let uctxs = Univ.ContextSet.of_context ctx in
+      Univ.ContextSet.to_context (Univ.ContextSet.union body_uctxs uctxs)
+    | Polymorphic_const ctx ->
+      assert(Univ.ContextSet.is_empty body_uctxs);
+      Univ.instantiate_univ_context ctx
 
 let universes_of_polymorphic_constant otab cb = 
-  if cb.const_polymorphic then 
-    let univs = universes_of_constant otab cb in
-      Univ.instantiate_univ_context univs
-  else Univ.UContext.empty
+  match cb.const_universes with
+  | Monomorphic_const _ -> Univ.UContext.empty
+  | Polymorphic_const ctx -> Univ.instantiate_univ_context ctx
 
 let constant_has_body cb = match cb.const_body with
   | Undef _ -> false
   | Def _ | OpaqueDef _ -> true
 
+let constant_polymorphic_instance cb =
+  match cb.const_universes with
+  | Monomorphic_const _ -> Univ.Instance.empty
+  | Polymorphic_const ctx -> Univ.AUContext.instance ctx
+
+let constant_polymorphic_context cb =
+  match cb.const_universes with
+  | Monomorphic_const _ -> Univ.UContext.empty
+  | Polymorphic_const ctx -> Univ.instantiate_univ_context ctx
+
 let is_opaque cb = match cb.const_body with
   | OpaqueDef _ -> true
   | Undef _ | Def _ -> false
@@ -142,7 +164,6 @@ let subst_const_body sub cb =
         const_proj = proj';
         const_body_code =
           Option.map (Cemitcodes.subst_to_patch_subst sub) cb.const_body_code;
-        const_polymorphic = cb.const_polymorphic;
         const_universes = cb.const_universes;
         const_inline_code = cb.const_inline_code;
         const_typing_flags = cb.const_typing_flags }
@@ -173,11 +194,18 @@ let hcons_const_def = function
     Def (from_val (Term.hcons_constr constr))
   | OpaqueDef _ as x -> x (* hashconsed when turned indirect *)
 
+let hcons_const_universes cbu =
+  match cbu with
+  | Monomorphic_const ctx -> 
+    Monomorphic_const (Univ.hcons_universe_context ctx)
+  | Polymorphic_const ctx -> 
+    Polymorphic_const (Univ.hcons_abstract_universe_context ctx)
+
 let hcons_const_body cb =
   { cb with
     const_body = hcons_const_def cb.const_body;
     const_type = hcons_const_type cb.const_type;
-    const_universes = Univ.hcons_universe_context cb.const_universes }
+    const_universes = hcons_const_universes cb.const_universes }
 
 (** {6 Inductive types } *)
 
@@ -266,22 +294,36 @@ let subst_mind_body sub mib =
     mind_params_ctxt =
       Context.Rel.map (subst_mps sub) mib.mind_params_ctxt;
     mind_packets = Array.smartmap (subst_mind_packet sub) mib.mind_packets ;
-    mind_polymorphic = mib.mind_polymorphic;
-    mind_cumulative = mib.mind_cumulative;
     mind_universes = mib.mind_universes;
     mind_private = mib.mind_private;
     mind_typing_flags = mib.mind_typing_flags;
   }
 
-let inductive_instance mib =
-  if mib.mind_polymorphic then
-    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 (Univ.UInfoInd.univ_context mib.mind_universes)
-  else Univ.UContext.empty
+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)
+
+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
 
 (** {6 Hash-consing of inductive declarations } *)
 
@@ -309,11 +351,17 @@ let hcons_mind_packet oib =
     mind_user_lc = user;
     mind_nf_lc = nf }
 
+let hcons_mind_universes miu =
+  match miu with
+  | Monomorphic_ind ctx -> Monomorphic_ind (Univ.hcons_universe_context ctx)
+  | Polymorphic_ind ctx -> Polymorphic_ind (Univ.hcons_abstract_universe_context ctx)
+  | Cumulative_ind cui -> Cumulative_ind (Univ.hcons_abstract_cumulativity_info cui)
+
 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_info_ind mib.mind_universes }
+    mind_universes = hcons_mind_universes mib.mind_universes }
 
 (** {6 Stm machinery } *)
 
diff --git a/kernel/declareops.mli b/kernel/declareops.mli
index 6650b6b7b..811a28aa6 100644
--- a/kernel/declareops.mli
+++ b/kernel/declareops.mli
@@ -27,6 +27,12 @@ val subst_const_body : substitution -> constant_body -> constant_body
 
 val constant_has_body : constant_body -> bool
 
+val constant_polymorphic_instance : constant_body -> universe_instance
+val constant_polymorphic_context : constant_body -> universe_context
+
+(** Is the constant polymorphic? *)
+val constant_is_polymorphic : constant_body -> bool
+
 (** Accessing const_body, forcing access to opaque proof term if needed.
     Only use this function if you know what you're doing. *)
 
@@ -66,8 +72,13 @@ val subst_wf_paths : substitution -> wf_paths -> wf_paths
 
 val subst_mind_body : substitution -> mutual_inductive_body -> mutual_inductive_body
 
-val inductive_instance : mutual_inductive_body -> universe_instance
-val inductive_context : mutual_inductive_body -> universe_context
+val inductive_polymorphic_instance : mutual_inductive_body -> universe_instance
+val inductive_polymorphic_context : mutual_inductive_body -> universe_context
+
+(** Is the inductive polymorphic? *)
+val inductive_is_polymorphic : mutual_inductive_body -> bool
+(** Is the inductive cumulative? *)
+val inductive_is_cumulative : mutual_inductive_body -> bool
 
 (** {6 Kernel flags} *)
 
diff --git a/kernel/entries.mli b/kernel/entries.mli
index 9c17346f2..f133587c1 100644
--- a/kernel/entries.mli
+++ b/kernel/entries.mli
@@ -34,6 +34,11 @@ then, in i{^ th} block, [mind_entry_params] is [xn:Xn;...;x1:X1];
 [mind_entry_lc] is [Ti1;...;Tini], defined in context [[A'1;...;A'p;x1:X1;...;xn:Xn]] where [A'i] is [Ai] generalized over [[x1:X1;...;xn:Xn]].
 *)
 
+type inductive_universes =
+  | Monomorphic_ind_entry of Univ.universe_context
+  | Polymorphic_ind_entry of Univ.universe_context
+  | Cumulative_ind_entry of Univ.cumulativity_info
+
 type one_inductive_entry = {
   mind_entry_typename : Id.t;
   mind_entry_arity : constr;
@@ -49,9 +54,7 @@ type mutual_inductive_entry = {
   mind_entry_finite : Decl_kinds.recursivity_kind;
   mind_entry_params : (Id.t * local_entry) list;
   mind_entry_inds : one_inductive_entry list;
-  mind_entry_polymorphic : bool;
-  mind_entry_cumulative : bool;
-  mind_entry_universes : Univ.universe_info_ind;
+  mind_entry_universes : inductive_universes;
   (* universe constraints and the constraints for subtyping of
      inductive types in the block. *)
   mind_entry_private : bool option;
diff --git a/kernel/environ.ml b/kernel/environ.ml
index 5727bf2ea..1ab5b7a8d 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -228,8 +228,10 @@ let add_constant kn cb env =
   add_constant_key kn cb no_link_info env
 
 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 -> 
@@ -240,15 +242,23 @@ 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)
+
+let constant_instance env kn =
+  let cb = lookup_constant kn env in
+  match cb.const_universes with
+  | Monomorphic_const _ -> Univ.Instance.empty
+  | Polymorphic_const ctx -> Univ.AUContext.instance ctx
 
 let constant_context env kn =
   let cb = lookup_constant kn env in
-    if cb.const_polymorphic then cb.const_universes
-    else Univ.UContext.empty
+  match cb.const_universes with
+  | Monomorphic_const _ -> Univ.UContext.empty
+  | Polymorphic_const ctx -> Univ.instantiate_univ_context ctx
 
 type const_evaluation_result = NoBody | Opaque | IsProj
 
@@ -259,10 +269,14 @@ let constant_value env (kn,u) =
     if cb.const_proj = None then
       match cb.const_body with
       | Def l_body -> 
-	if cb.const_polymorphic then
-	  let csts = constraints_of cb u in
-	    (subst_instance_constr u (Mod_subst.force_constr l_body), csts)
-	else Mod_subst.force_constr l_body, Univ.Constraint.empty
+        begin
+          match cb.const_universes with
+          | Monomorphic_const _ -> 
+            (Mod_subst.force_constr l_body, Univ.Constraint.empty)
+          | Polymorphic_const _ ->
+	    let csts = constraints_of cb u in
+            (subst_instance_constr u (Mod_subst.force_constr l_body), csts)
+        end
       | OpaqueDef _ -> raise (NotEvaluableConst Opaque)
       | Undef _ -> raise (NotEvaluableConst NoBody)
     else raise (NotEvaluableConst IsProj)
@@ -273,7 +287,7 @@ let constant_opt_value env cst =
 
 let constant_value_and_type env (kn, u) =
   let cb = lookup_constant kn env in
-    if cb.const_polymorphic then
+    if Declareops.constant_is_polymorphic cb then
       let cst = constraints_of cb u in
       let b' = match cb.const_body with
 	| Def l_body -> Some (subst_instance_constr u (Mod_subst.force_constr l_body))
@@ -295,7 +309,7 @@ let constant_value_and_type env (kn, u) =
 (* constant_type gives the type of a constant *)
 let constant_type_in env (kn,u) =
   let cb = lookup_constant kn env in
-    if cb.const_polymorphic then
+    if Declareops.constant_is_polymorphic cb then
       map_regular_arity (subst_instance_constr u) cb.const_type
     else cb.const_type
 
@@ -321,7 +335,7 @@ let evaluable_constant kn env =
     | Undef _ -> false
 
 let polymorphic_constant cst env =
-  (lookup_constant cst env).const_polymorphic
+  Declareops.constant_is_polymorphic (lookup_constant cst env)
 
 let polymorphic_pconstant (cst,u) env =
   if Univ.Instance.is_empty u then false
@@ -353,7 +367,7 @@ let is_projection cst env =
 let lookup_mind = lookup_mind
 
 let polymorphic_ind (mind,i) env =
-  (lookup_mind mind env).mind_polymorphic
+  Declareops.inductive_is_polymorphic (lookup_mind mind env)
 
 let polymorphic_pind (ind,u) env =
   if Univ.Instance.is_empty u then false
diff --git a/kernel/environ.mli b/kernel/environ.mli
index b7431dbe5..ae3afcb35 100644
--- a/kernel/environ.mli
+++ b/kernel/environ.mli
@@ -161,6 +161,9 @@ val constant_value_and_type : env -> constant puniverses ->
 (** The universe context associated to the constant, empty if not 
     polymorphic *)
 val constant_context : env -> constant -> Univ.universe_context
+(** The universe isntance associated to the constant, empty if not 
+    polymorphic *)
+val constant_instance : env -> constant -> Univ.universe_instance
 
 (* These functions should be called under the invariant that [env] 
    already contains the constraints corresponding to the constant 
@@ -256,7 +259,7 @@ type unsafe_type_judgment = types punsafe_type_judgment
 
 (** {6 Compilation of global declaration } *)
 
-val compile_constant_body : env -> constant_universes option -> constant_def -> Cemitcodes.body_code option
+val compile_constant_body : env -> constant_universes -> constant_def -> Cemitcodes.body_code option
 
 exception Hyp_not_found
 
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index 5cfcbba60..00fbe27a7 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -231,23 +231,23 @@ let check_subtyping_arity_constructor env (subst : constr -> constr) (arcn : Ter
 
 (* 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 mie paramsctxt env_ar inds = 
+let check_subtyping cumi paramsctxt env_ar inds = 
     let numparams = Context.Rel.nhyps paramsctxt in
-    let sbsubst = UInfoInd.subtyping_susbst mie.mind_entry_universes in
+    let sbsubst = CumulativityInfo.subtyping_susbst cumi in
     let dosubst = subst_univs_level_constr sbsubst in
-    let uctx = UInfoInd.univ_context mie.mind_entry_universes in
+    let uctx = CumulativityInfo.univ_context cumi in
     let instance_other = Univ.subst_univs_level_instance sbsubst (Univ.UContext.instance uctx) in
     let constraints_other = Univ.subst_univs_level_constraints sbsubst (Univ.UContext.constraints uctx) in
     let uctx_other = Univ.UContext.make (instance_other, constraints_other) in
-    let env' = Environ.push_context uctx env_ar in
-    let env'' = Environ.push_context uctx_other env' in
-    let envsb = push_context (UInfoInd.subtyp_context mie.mind_entry_universes) env'' in
+    let env = Environ.push_context uctx env_ar in
+    let env = Environ.push_context uctx_other env in
+    let env = push_context (CumulativityInfo.subtyp_context cumi) env in
     (* process individual inductive types: *)
     Array.iter (fun (id,cn,lc,(sign,arity)) ->
       match arity with
         | RegularArity (_, full_arity, _) ->
-           check_subtyping_arity_constructor envsb dosubst full_arity numparams true;
-           Array.iter (fun cnt -> check_subtyping_arity_constructor envsb dosubst cnt numparams false) lc
+           check_subtyping_arity_constructor env dosubst full_arity numparams true;
+           Array.iter (fun cnt -> check_subtyping_arity_constructor env dosubst cnt numparams false) lc
         | TemplateArity _ -> ()
     ) inds
 
@@ -264,7 +264,13 @@ let typecheck_inductive env mie =
   (* Check unicity of names *)
   mind_check_names mie;
   (* Params are typed-checked here *)
-  let env' = push_context (Univ.UInfoInd.univ_context mie.mind_entry_universes) env in
+  let univctx =
+    match mie.mind_entry_universes with
+    | Monomorphic_ind_entry ctx -> ctx
+    | Polymorphic_ind_entry ctx -> ctx
+    | Cumulative_ind_entry cumi -> Univ.CumulativityInfo.univ_context cumi
+  in
+  let env' = push_context univctx 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 *)
@@ -383,16 +389,21 @@ let typecheck_inductive env mie =
 	  | _ (* Not an explicit occurrence of Type *) ->
 	    full_polymorphic ()
       in
-      let arity = 
-	if mie.mind_entry_polymorphic then full_polymorphic ()
-	else template_polymorphic ()
+      let arity =
+        match mie.mind_entry_universes with
+        | Monomorphic_ind_entry _ -> template_polymorphic ()
+        | Polymorphic_ind_entry _ | Cumulative_ind_entry _ -> full_polymorphic ()
       in
 	(id,cn,lc,(sign,arity)))
     inds
   in
   (* 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 () = if mie.mind_entry_cumulative then check_subtyping mie paramsctxt env_arities inds
+  let () = 
+    match mie.mind_entry_universes with
+    | Monomorphic_ind_entry _ -> ()
+    | Polymorphic_ind_entry _ -> ()
+    | Cumulative_ind_entry cumi -> check_subtyping cumi paramsctxt env_arities inds
   in (env_arities, env_ar_par, paramsctxt, inds)
 
 (************************************************************************)
@@ -864,14 +875,21 @@ let compute_projections ((kn, _ as ind), u as indu) n x nparamargs params
     Array.of_list (List.rev kns),
     Array.of_list (List.rev pbs)
 
-let build_inductive env cum p prv ctx env_ar paramsctxt kn isrecord isfinite inds nmr recargs =
+let abstract_inductive_universes iu =
+  match iu with
+  | Monomorphic_ind_entry ctx -> (Univ.empty_level_subst, Monomorphic_ind ctx)
+  | Polymorphic_ind_entry ctx -> 
+    let (inst, auctx) = Univ.abstract_universes ctx in (inst, Polymorphic_ind auctx)
+  | Cumulative_ind_entry cumi -> 
+    let (inst, acumi) = Univ.abstract_cumulativity_info cumi in (inst, Cumulative_ind acumi)
+
+let build_inductive env prv iu env_ar paramsctxt kn isrecord isfinite inds nmr recargs =
   let ntypes = Array.length inds in
   (* Compute the set of used section variables *)
   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 (Univ.UInfoInd.univ_context ctx) in
-  let substsubtyp, ctxsubtyp = Univ.abstract_universes p (Univ.UInfoInd.subtyp_context ctx) in
+  let substunivs, aiu = abstract_inductive_universes iu in
   let paramsctxt = Vars.subst_univs_level_context substunivs paramsctxt in
   let env_ar =
     let ctxunivs = Environ.rel_context env_ar in 
@@ -942,10 +960,14 @@ let build_inductive env cum p prv ctx env_ar paramsctxt kn isrecord isfinite ind
 			   && Array.length pkt.mind_consnames == 1
 			   && pkt.mind_consnrealargs.(0) > 0 ->
       (** The elimination criterion ensures that all projections can be defined. *)
-      let u = 
-	if p then 
-	  subst_univs_level_instance substunivs (Univ.UContext.instance ctxunivs)
-	else Univ.Instance.empty 
+      let u =
+        let process auctx = 
+          subst_univs_level_instance substunivs (Univ.AUContext.instance auctx)
+        in
+        match aiu with
+        | Monomorphic_ind _ -> Univ.Instance.empty
+        | Polymorphic_ind auctx -> process auctx
+        | Cumulative_ind acumi -> process (Univ.ACumulativityInfo.univ_context acumi)
       in
       let indsp = ((kn, 0), u) in
       let rctx, indty = decompose_prod_assum (subst1 (mkIndU indsp) pkt.mind_nf_lc.(0)) in
@@ -968,9 +990,7 @@ let build_inductive env cum p prv ctx env_ar paramsctxt kn isrecord isfinite ind
       mind_nparams_rec = nmr;
       mind_params_ctxt = paramsctxt;
       mind_packets = packets;
-      mind_polymorphic = p;
-      mind_cumulative = cum;
-      mind_universes = Univ.UInfoInd.make (ctxunivs, ctxsubtyp);
+      mind_universes = aiu;
       mind_private = prv;
       mind_typing_flags = Environ.typing_flags env;
     }
@@ -985,7 +1005,6 @@ let check_inductive env kn mie =
   let chkpos = (Environ.typing_flags env).check_guarded in
   let (nmr,recargs) = check_positivity ~chkpos kn env_ar_par paramsctxt mie.mind_entry_finite inds in
   (* Build the inductive packets *)
-    build_inductive env mie.mind_entry_cumulative mie.mind_entry_polymorphic mie.mind_entry_private
-      mie.mind_entry_universes
+    build_inductive env mie.mind_entry_private mie.mind_entry_universes
       env_ar paramsctxt kn mie.mind_entry_record mie.mind_entry_finite
       inds nmr recargs
diff --git a/kernel/indtypes.mli b/kernel/indtypes.mli
index 7b0f01794..5b4615399 100644
--- a/kernel/indtypes.mli
+++ b/kernel/indtypes.mli
@@ -32,17 +32,6 @@ type inductive_error =
 
 exception InductiveError of inductive_error
 
-val check_subtyping_arity_constructor : Environ.env ->
-(Term.constr -> Term.constr) -> Term.types -> int -> bool -> unit
-
-(* This needs not be exposed. Exposing for debugging purposes! *)
-val check_subtyping : Entries.mutual_inductive_entry ->
-Context.Rel.t ->
-Environ.env ->
-('b * 'c * Term.types array *
- ('d * ('e * Term.types * 'f, 'g) Declarations.declaration_arity))
-array -> unit
-
 (** The following function does checks on inductive declarations. *)
 
 val check_inductive : env -> mutual_inductive -> mutual_inductive_entry -> mutual_inductive_body
diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index 0f0dc0d60..e81a1cb58 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -54,9 +54,13 @@ let inductive_paramdecls (mib,u) =
   Vars.subst_instance_context u mib.mind_params_ctxt
 
 let instantiate_inductive_constraints mib u =
-  if mib.mind_polymorphic then
-    Univ.subst_instance_constraints u (Univ.UContext.constraints (Univ.UInfoInd.univ_context mib.mind_universes))
-  else Univ.Constraint.empty
+  let process auctx = 
+    Univ.UContext.constraints (Univ.subst_instance_context u auctx)
+  in
+  match mib.mind_universes with
+  | Monomorphic_ind _ -> Univ.Constraint.empty
+  | Polymorphic_ind auctx -> process auctx
+  | Cumulative_ind cumi -> process (Univ.ACumulativityInfo.univ_context cumi)
 
 
 (************************************************************************)
diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml
index ff44f0f54..79016735b 100644
--- a/kernel/mod_typing.ml
+++ b/kernel/mod_typing.ml
@@ -74,12 +74,13 @@ let rec check_with_def env struc (idl,(c,ctx)) mp equiv =
 	 as long as they have the right type *)
       let uctx = Declareops.universes_of_constant (opaque_tables env) cb in
       let uctx = (* Context of the spec *)
-	if cb.const_polymorphic then
-	  Univ.instantiate_univ_context uctx
-	else uctx
+        match cb.const_universes with
+        | Monomorphic_const _ -> uctx
+        | Polymorphic_const auctx ->
+	  Univ.instantiate_univ_context auctx
       in
       let c', univs, ctx' = 
-	if not cb.const_polymorphic then
+	if not (Declareops.constant_is_polymorphic cb) then
 	  let env' = Environ.push_context ~strict:true uctx env' in
 	  let env' = Environ.push_context ~strict:true ctx env' in
 	  let c',cst = match cb.const_body with
@@ -92,7 +93,7 @@ let rec check_with_def env struc (idl,(c,ctx)) mp equiv =
 	    | Def cs ->
 	       let c' = Mod_subst.force_constr cs in
 	         c, Reduction.infer_conv env' (Environ.universes env') c c'
-	  in c', ctx, Univ.ContextSet.add_constraints cst (Univ.ContextSet.of_context ctx)
+	  in c', Monomorphic_const ctx, Univ.ContextSet.add_constraints cst (Univ.ContextSet.of_context ctx)
 	else
 	  let cus, ccst = Univ.UContext.dest uctx in
 	  let newus, cst = Univ.UContext.dest ctx in
@@ -122,21 +123,17 @@ let rec check_with_def env struc (idl,(c,ctx)) mp equiv =
 	  in
 	    if not (Univ.Constraint.is_empty cst) then
 	      error_incorrect_with_constraint lab;
-	    let subst, ctx = Univ.abstract_universes true ctx in
-	      Vars.subst_univs_level_constr subst c, ctx, Univ.ContextSet.empty
+	    let subst, ctx = Univ.abstract_universes ctx in
+	      Vars.subst_univs_level_constr subst c, Polymorphic_const ctx, Univ.ContextSet.empty
       in
       let def = Def (Mod_subst.from_val c') in
 (*      let ctx' = Univ.UContext.make (newus, cst) in *)
-      let univs =
-        if cb.const_polymorphic then Some cb.const_universes
-        else None
-      in
       let cb' =
 	{ cb with
 	  const_body = def;
-          const_universes = ctx ;
+          const_universes = univs ;
 	  const_body_code = Option.map Cemitcodes.from_val
-                              (compile_constant_body env' univs def) }
+                              (compile_constant_body env' cb.const_universes def) }
       in
       before@(lab,SFBconst(cb'))::after, c', ctx'
     else
diff --git a/kernel/modops.ml b/kernel/modops.ml
index 1f8b97ae6..33d13f1ba 100644
--- a/kernel/modops.ml
+++ b/kernel/modops.ml
@@ -35,6 +35,7 @@ type signature_mismatch_error =
   | NotConvertibleConstructorField of Id.t
   | NotConvertibleBodyField
   | NotConvertibleTypeField of env * types * types
+  | CumulativeStatusExpected of bool
   | PolymorphicStatusExpected of bool
   | NotSameConstructorNamesField
   | NotSameInductiveNameInBlockField
@@ -327,12 +328,10 @@ let strengthen_const mp_from l cb resolver =
   |_ ->
     let kn = KerName.make2 mp_from l in
     let con = constant_of_delta_kn resolver kn in
-    let u = 
-      if cb.const_polymorphic then
-	let u = Univ.UContext.instance cb.const_universes in
-	let s = Univ.make_instance_subst u in
-	  Univ.subst_univs_level_instance s u
-      else Univ.Instance.empty
+    let u =
+      match cb.const_universes with
+      | Monomorphic_const _ -> Univ.Instance.empty
+      | Polymorphic_const ctx -> Univ.make_abstract_instance ctx
     in
       { cb with
 	const_body = Def (Mod_subst.from_val (mkConstU (con,u)));
diff --git a/kernel/modops.mli b/kernel/modops.mli
index e9f3db6e9..4b533c7ef 100644
--- a/kernel/modops.mli
+++ b/kernel/modops.mli
@@ -94,6 +94,7 @@ type signature_mismatch_error =
   | NotConvertibleConstructorField of Id.t
   | NotConvertibleBodyField
   | NotConvertibleTypeField of env * types * types
+  | CumulativeStatusExpected of bool
   | PolymorphicStatusExpected of bool
   | NotSameConstructorNamesField
   | NotSameInductiveNameInBlockField
diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml
index d3cd6b62a..4941d64d8 100644
--- a/kernel/nativecode.ml
+++ b/kernel/nativecode.ml
@@ -1863,8 +1863,9 @@ let compile_constant env sigma prefix ~interactive con cb =
   match cb.const_proj with
   | None ->
      let u =
-       if cb.const_polymorphic then Univ.UContext.instance cb.const_universes
-       else Univ.Instance.empty
+       match cb.const_universes with
+       | Monomorphic_const _ -> Univ.Instance.empty
+       | Polymorphic_const ctx -> Univ.AUContext.instance ctx
      in
     begin match cb.const_body with
     | Def t ->
@@ -1960,7 +1961,7 @@ let param_name = Name (id_of_string "params")
 let arg_name = Name (id_of_string "arg")
 
 let compile_mind prefix ~interactive mb mind stack =
-  let u = Declareops.inductive_instance mb in
+  let u = Declareops.inductive_polymorphic_instance mb in
   let f i stack ob =
     let gtype = Gtype((mind, i), Array.map snd ob.mind_reloc_tbl) in
     let j = push_symbol (SymbInd (mind,i)) in
diff --git a/kernel/opaqueproof.ml b/kernel/opaqueproof.ml
index 59e90ca2e..3e15ff740 100644
--- a/kernel/opaqueproof.ml
+++ b/kernel/opaqueproof.ml
@@ -16,7 +16,7 @@ type work_list = (Instance.t * Id.t array) Cmap.t *
 
 type cooking_info = { 
   modlist : work_list; 
-  abstract : Context.Named.t * Univ.universe_level_subst * Univ.UContext.t } 
+  abstract : Context.Named.t * Univ.universe_level_subst * Univ.AUContext.t } 
 type proofterm = (constr * Univ.universe_context_set) Future.computation
 type opaque =
   | Indirect of substitution list * DirPath.t * int (* subst, lib, index *)
diff --git a/kernel/opaqueproof.mli b/kernel/opaqueproof.mli
index 3897d5e51..be1f4b13f 100644
--- a/kernel/opaqueproof.mli
+++ b/kernel/opaqueproof.mli
@@ -49,7 +49,7 @@ type work_list = (Univ.Instance.t * Id.t array) Cmap.t *
 
 type cooking_info = { 
   modlist : work_list; 
-  abstract : Context.Named.t * Univ.universe_level_subst * Univ.UContext.t } 
+  abstract : Context.Named.t * Univ.universe_level_subst * Univ.AUContext.t } 
 
 (* The type has two caveats:
    1) cook_constr is defined after
diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index ea583fdac..8bf95e5de 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -497,11 +497,12 @@ and eqappr env cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv =
       if eq_ind ind1 ind2 then
         let mind = Environ.lookup_mind (fst ind1) env in
         let cuniv =
-          if mind.Declarations.mind_polymorphic && mind.Declarations.mind_cumulative then
+          match mind.Declarations.mind_universes with
+          | Declarations.Monomorphic_ind _ | Declarations.Polymorphic_ind _ ->
+            convert_instances ~flex:false u1 u2 cuniv
+          | Declarations.Cumulative_ind cumi ->
             convert_inductives cv_pb (mind, snd ind1) u1 (CClosure.stack_args_size v1)
               u2 (CClosure.stack_args_size v2) cuniv
-          else
-            convert_instances ~flex:false u1 u2 cuniv
         in
         convert_stacks env l2r infos lft1 lft2 v1 v2 cuniv
       else raise NotConvertible
@@ -510,12 +511,13 @@ and eqappr env cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv =
       if Int.equal j1 j2 && eq_ind ind1 ind2 then
         let mind = Environ.lookup_mind (fst ind1) env in
         let cuniv =
-          if mind.Declarations.mind_polymorphic && mind.Declarations.mind_cumulative then
+          match mind.Declarations.mind_universes with
+          | Declarations.Monomorphic_ind _ | Declarations.Polymorphic_ind _ ->
+            convert_instances ~flex:false u1 u2 cuniv
+          | Declarations.Cumulative_ind _ ->
             convert_constructors
               (mind, snd ind1, j1) u1 (CClosure.stack_args_size v1)
               u2 (CClosure.stack_args_size v2) cuniv
-          else
-            convert_instances ~flex:false u1 u2 cuniv
         in
         convert_stacks env l2r infos lft1 lft2 v1 v2 cuniv
       else raise NotConvertible
@@ -637,22 +639,26 @@ let infer_check_conv_inductives
     infer_check_convert_instances
     infer_check_inductive_instances
     cv_pb (mind, ind) u1 sv1 u2 sv2 univs =
-  if mind.Declarations.mind_polymorphic then
+  match mind.Declarations.mind_universes with
+  | Declarations.Monomorphic_ind _ | Declarations.Polymorphic_ind _ ->
+    infer_check_convert_instances ~flex:false u1 u2 univs
+  | Declarations.Cumulative_ind cumi ->
     let num_param_arity =
       mind.Declarations.mind_nparams + mind.Declarations.mind_packets.(ind).Declarations.mind_nrealargs
     in
     if not (num_param_arity = sv1 && num_param_arity = sv2) then
       infer_check_convert_instances ~flex:false u1 u2 univs
     else
-      let uinfind = mind.Declarations.mind_universes in
-      infer_check_inductive_instances cv_pb uinfind u1 u2 univs
-  else infer_check_convert_instances ~flex:false u1 u2 univs
+      infer_check_inductive_instances cv_pb cumi u1 u2 univs
 
 let infer_check_conv_constructors
     infer_check_convert_instances
     infer_check_inductive_instances
     (mind, ind, cns) u1 sv1 u2 sv2 univs =
-  if mind.Declarations.mind_polymorphic then
+  match mind.Declarations.mind_universes with
+  | Declarations.Monomorphic_ind _ | Declarations.Polymorphic_ind _ ->
+    infer_check_convert_instances ~flex:false u1 u2 univs
+  | Declarations.Cumulative_ind cumi ->
     let num_cnstr_args =
       let nparamsctxt =
         mind.Declarations.mind_nparams + mind.Declarations.mind_packets.(ind).Declarations.mind_nrealargs
@@ -662,26 +668,30 @@ let infer_check_conv_constructors
     if not (num_cnstr_args = sv1 && num_cnstr_args = sv2) then
       infer_check_convert_instances ~flex:false u1 u2 univs
     else
-      let uinfind = mind.Declarations.mind_universes in
-      infer_check_inductive_instances CONV uinfind u1 u2 univs
-  else infer_check_convert_instances ~flex:false u1 u2 univs
+      infer_check_inductive_instances CONV cumi u1 u2 univs
 
-let check_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 check_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!")
   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
@@ -746,22 +756,27 @@ let infer_convert_instances ~flex u u' (univs,cstrs) =
     else Univ.enforce_eq_instances u u' cstrs
   in (univs, cstrs')
 
-let infer_inductive_instances cv_pb uinfind u u' (univs, cstrs) =
-  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 infer_inductive_instances cv_pb cumi u u' (univs, cstrs) =
+  let ind_instance = 
+    Univ.AUContext.instance (Univ.ACumulativityInfo.subtyp_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!")
   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
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 1568fe0bf..946222ef2 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -237,20 +237,29 @@ let private_con_of_scheme ~kind env cl =
 
 let universes_of_private eff =
   let open Declarations in
-  List.fold_left (fun acc { Entries.eff } ->
-     match eff with
-     | Entries.SEscheme (l,s) ->
-        List.fold_left (fun acc (_,_,cb,c) ->
-          let acc = match c with
-            | `Nothing -> acc
-            | `Opaque (_, ctx) -> ctx :: acc in
-          if cb.const_polymorphic then acc
-          else (Univ.ContextSet.of_context cb.const_universes) :: acc)
-        acc l
-     | Entries.SEsubproof (c, cb, e) ->
-	if cb.const_polymorphic then acc
-	else Univ.ContextSet.of_context cb.const_universes :: acc)
-   [] (Term_typing.uniq_seff eff)
+  List.fold_left
+    (fun acc { Entries.eff } ->
+       match eff with
+       | Entries.SEscheme (l,s) ->
+         List.fold_left
+           (fun acc (_,_,cb,c) ->
+              let acc = match c with
+                | `Nothing -> acc
+                | `Opaque (_, ctx) -> ctx :: acc
+              in
+              match cb.const_universes with
+              | Monomorphic_const ctx ->
+                (Univ.ContextSet.of_context ctx) :: acc
+              | Polymorphic_const _ -> acc
+           )
+           acc l
+       | Entries.SEsubproof (c, cb, e) ->
+         match cb.const_universes with
+              | Monomorphic_const ctx ->
+                (Univ.ContextSet.of_context ctx) :: acc
+              | Polymorphic_const _ -> acc
+    )
+    [] (Term_typing.uniq_seff eff)
 
 let env_of_safe_env senv = senv.env
 let env_of_senv = env_of_safe_env
@@ -373,7 +382,11 @@ let safe_push_named d env =
 
 
 let push_named_def (id,de) senv =
-  let c,typ,univs = Term_typing.translate_local_def senv.revstruct senv.env id de in
+  let c,typ,univs = 
+    match Term_typing.translate_local_def senv.revstruct senv.env id de with
+    | c, typ, Monomorphic_const ctx -> c, typ, ctx
+    | _, _, Polymorphic_const _ -> assert false
+  in
   let poly = de.Entries.const_entry_polymorphic in
   let univs = Univ.ContextSet.of_context univs in
   let c, univs = match c with
@@ -410,26 +423,28 @@ let labels_of_mib mib =
   get ()
 
 let globalize_constant_universes env cb =
-  if cb.const_polymorphic then
-    [Now (true, Univ.ContextSet.empty)]
-  else
-    let cstrs = Univ.ContextSet.of_context cb.const_universes in
-      Now (false, cstrs) ::  
-	(match cb.const_body with
-	| (Undef _ | Def _) -> []
-	| OpaqueDef lc ->
-	  match Opaqueproof.get_constraints (Environ.opaque_tables env) lc with
-	  | None -> []
-	  | Some fc ->
+  match cb.const_universes with
+  | Monomorphic_const ctx ->
+    let cstrs = Univ.ContextSet.of_context ctx in
+    Now (false, cstrs) ::  
+    (match cb.const_body with
+     | (Undef _ | Def _) -> []
+     | OpaqueDef lc ->
+       match Opaqueproof.get_constraints (Environ.opaque_tables env) lc with
+       | None -> []
+       | Some fc ->
             match Future.peek_val fc with
-            | None -> [Later fc]
-            | Some c -> [Now (false, c)])
+             | None -> [Later fc]
+             | Some c -> [Now (false, c)])
+  | Polymorphic_const _ ->
+    [Now (true, Univ.ContextSet.empty)]
       
 let globalize_mind_universes mb =
-  if mb.mind_polymorphic then
-    [Now (true, Univ.ContextSet.empty)]
-  else
-    [Now (false, Univ.ContextSet.of_context (Univ.UInfoInd.univ_context mb.mind_universes))]
+  match mb.mind_universes with
+  | Monomorphic_ind ctx ->
+    [Now (false, Univ.ContextSet.of_context ctx)]
+  | Polymorphic_ind _ -> [Now (true, Univ.ContextSet.empty)]
+  | Cumulative_ind _ -> [Now (true, Univ.ContextSet.empty)]
 
 let constraints_of_sfb env sfb = 
   match sfb with
diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml
index 60e630a6d..1bd9d6e49 100644
--- a/kernel/subtyping.ml
+++ b/kernel/subtyping.ml
@@ -104,15 +104,21 @@ let check_inductive cst env mp1 l info1 mp2 mib2 spec2 subst1 subst2 reso1 reso2
       | IndType ((_,0), mib) -> Declareops.subst_mind_body subst1 mib
       | _ -> error (InductiveFieldExpected mib2)
   in
-  let poly = 
-    if not (mib1.mind_polymorphic == mib2.mind_polymorphic) then
-      error (PolymorphicStatusExpected mib2.mind_polymorphic)
-    else mib2.mind_polymorphic
-  in
-  let u = 
-    if poly then 
-      CErrors.user_err Pp.(str "Checking of subtyping of polymorphic inductive types not implemented")
-    else Instance.empty
+  let u =
+    let process inst inst' =
+      if Univ.Instance.equal inst inst' then inst else error IncompatibleInstances
+    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 
+             (CumulativeStatusExpected (Declareops.inductive_is_cumulative mib2))
   in
   let mib2 =  Declareops.subst_mind_body subst2 mib2 in
   let check_inductive_type cst name env t1 t2 =
@@ -148,7 +154,7 @@ let check_inductive cst env mp1 l info1 mp2 mib2 spec2 subst1 subst2 reso1 reso2
 	error (NotConvertibleInductiveField name)
       | _ -> (s1, s2) in
     check_conv (NotConvertibleInductiveField name)
-      cst poly u infer_conv_leq env (mkArity (ctx1,s1)) (mkArity (ctx2,s2))
+      cst (inductive_is_polymorphic mib1) u infer_conv_leq env (mkArity (ctx1,s1)) (mkArity (ctx2,s2))
   in
 
   let check_packet cst p1 p2 =
@@ -176,7 +182,7 @@ let check_inductive cst env mp1 l info1 mp2 mib2 spec2 subst1 subst2 reso1 reso2
   let check_cons_types i cst p1 p2 =
     Array.fold_left3
       (fun cst id t1 t2 -> check_conv (NotConvertibleConstructorField id) cst
-	poly u infer_conv env t1 t2)
+	(inductive_is_polymorphic mib1) u infer_conv env t1 t2)
       cst
       p2.mind_consnames
       (arities_of_specif (mind,u) (mib1,p1))
@@ -293,37 +299,42 @@ let check_constant cst env mp1 l info1 cb2 spec2 subst1 subst2 =
       let cb2 = Declareops.subst_const_body subst2 cb2 in
       (* Start by checking universes *)
       let poly = 
-	if not (cb1.const_polymorphic == cb2.const_polymorphic) then
-	  error (PolymorphicStatusExpected cb2.const_polymorphic)
-	else cb2.const_polymorphic
+	if not (Declareops.constant_is_polymorphic cb1 
+                 == Declareops.constant_is_polymorphic cb2) then
+           error (PolymorphicStatusExpected (Declareops.constant_is_polymorphic cb2))
+	else Declareops.constant_is_polymorphic cb2
       in
-      let cst', env', u = 
-	if poly then 
-	  let ctx1 = Univ.instantiate_univ_context cb1.const_universes in
-	  let ctx2 = Univ.instantiate_univ_context cb2.const_universes in
-	  let inst1, ctx1 = Univ.UContext.dest ctx1 in
-	  let inst2, ctx2 = Univ.UContext.dest ctx2 in
+      let cst', env', u =
+        match cb1.const_universes, cb2.const_universes with
+        | Monomorphic_const _, Monomorphic_const _ ->
+          cst, env, Univ.Instance.empty
+        | Polymorphic_const auctx1, Polymorphic_const auctx2 ->
+          begin
+	    let ctx1 = Univ.instantiate_univ_context auctx1 in
+	    let ctx2 = Univ.instantiate_univ_context auctx2 in
+	    let inst1, ctx1 = Univ.UContext.dest ctx1 in
+	    let inst2, ctx2 = Univ.UContext.dest ctx2 in
 	    if not (Univ.Instance.length inst1 == Univ.Instance.length inst2) then
 	      error IncompatibleInstances
 	    else 
 	      let cstrs = Univ.enforce_eq_instances inst1 inst2 cst in
 	      let cstrs = Univ.Constraint.union cstrs ctx2 in
-		try 
-		  (* The environment with the expected universes plus equality 
-		     of the body instances with the expected instance *)
-		  let ctxi = Univ.Instance.append inst1 inst2 in
-		  let ctx = Univ.UContext.make (ctxi, cstrs) in
-		  let env = Environ.push_context ctx env in
-		  (* Check that the given definition does not add any constraint over
-		     the expected ones, so that it can be used in place of 
-                     the original. *)
-		    if UGraph.check_constraints ctx1 (Environ.universes env) then
-		      cstrs, env, inst2
-		    else error (IncompatibleConstraints ctx1)
-		with Univ.UniverseInconsistency incon -> 
-		  error (IncompatibleUniverses incon)
-	else
-	  cst, env, Univ.Instance.empty
+	      try 
+		(* The environment with the expected universes plus equality 
+		   of the body instances with the expected instance *)
+		let ctxi = Univ.Instance.append inst1 inst2 in
+		let ctx = Univ.UContext.make (ctxi, cstrs) in
+		let env = Environ.push_context ctx env in
+		(* Check that the given definition does not add any constraint over
+		   the expected ones, so that it can be used in place of 
+                                 the original. *)
+		if UGraph.check_constraints ctx1 (Environ.universes env) then
+		  cstrs, env, inst2
+		else error (IncompatibleConstraints ctx1)
+	      with Univ.UniverseInconsistency incon -> 
+		error (IncompatibleUniverses incon)
+          end
+        | _ -> assert false
       in
       (* Now check types *)
       let typ1 = Typeops.type_of_constant_type env' cb1.const_type in
@@ -354,7 +365,7 @@ let check_constant cst env mp1 l info1 cb2 spec2 subst1 subst2 =
        "name."));
       let () = assert (List.is_empty mind1.mind_hyps && List.is_empty cb2.const_hyps) in
       if Declareops.constant_has_body cb2 then error DefinitionFieldExpected;
-      let u1 = inductive_instance mind1 in
+      let u1 = inductive_polymorphic_instance mind1 in
       let arity1,cst1 = constrained_type_of_inductive env 
 	((mind1,mind1.mind_packets.(i)),u1) in
       let cst2 =
@@ -371,7 +382,7 @@ let check_constant cst env mp1 l info1 cb2 spec2 subst1 subst2 =
        "name."));
       let () = assert (List.is_empty mind1.mind_hyps && List.is_empty cb2.const_hyps) in
       if Declareops.constant_has_body cb2 then error DefinitionFieldExpected;
-      let u1 = inductive_instance mind1 in
+      let u1 = inductive_polymorphic_instance mind1 in
       let ty1,cst1 = constrained_type_of_constructor (cstr,u1) (mind1,mind1.mind_packets.(i)) in
       let cst2 =
         Declareops.constraints_of_constant (Environ.opaque_tables env) cb2 in
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index 3cf2299d8..5370bcea4 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -121,18 +121,19 @@ let inline_side_effects env body ctx side_eff =
       | OpaqueDef _, `Opaque (b,_) -> (b, true)
       | _ -> assert false
       in
-      if cb.const_polymorphic then
-        (** Inline the term to emulate universe polymorphism *)
-        let data = (Univ.UContext.instance cb.const_universes, b) in
-        let subst = Cmap_env.add c (Inl data) subst in
-        (subst, var, ctx, args)
-      else
+      match cb.const_universes with
+      | Monomorphic_const cnstctx ->
         (** Abstract over the term at the top of the proof *)
         let ty = Typeops.type_of_constant_type env cb.const_type in
         let subst = Cmap_env.add c (Inr var) subst in
-        let univs = Univ.ContextSet.of_context cb.const_universes in
+        let univs = Univ.ContextSet.of_context cnstctx in
         let ctx = Univ.ContextSet.union ctx univs in
         (subst, var + 1, ctx, (cname c, b, ty, opaque) :: args)
+      | Polymorphic_const auctx ->
+        (** Inline the term to emulate universe polymorphism *)
+        let data = (Univ.AUContext.instance auctx, b) in
+        let subst = Cmap_env.add c (Inl data) subst in
+        (subst, var, ctx, args)
     in
     let (subst, len, ctx, args) = List.fold_left fold (Cmap_env.empty, 1, ctx, []) side_eff in
     (** Third step: inline the definitions *)
@@ -225,16 +226,25 @@ let feedback_completion_typecheck =
   Option.iter (fun state_id ->
       feedback ~id:state_id Feedback.Complete)
 
+let abstract_constant_universes abstract uctx =
+  if not abstract then
+    Univ.empty_level_subst, Monomorphic_const uctx
+  else
+    let sbst, auctx = Univ.abstract_universes uctx in
+    sbst, Polymorphic_const auctx
+
 let infer_declaration ~trust env kn dcl =
   match dcl with
   | ParameterEntry (ctx,poly,(t,uctx),nl) ->
       let env = push_context ~strict:(not poly) uctx env in
       let j = infer env t in
       let abstract = poly && not (Option.is_empty kn) in
-      let usubst, univs = Univ.abstract_universes abstract uctx in
+      let usubst, univs = 
+        abstract_constant_universes abstract uctx
+      in
       let c = Typeops.assumption_of_judgment env j in
       let t = hcons_constr (Vars.subst_univs_level_constr usubst c) in
-	Undef nl, RegularArity t, None, poly, univs, false, ctx
+	Undef nl, RegularArity t, None, univs, false, ctx
 
   (** Definition [c] is opaque (Qed), non polymorphic and with a specified type,
       so we delay the typing and hash consing of its body.
@@ -264,9 +274,9 @@ let infer_declaration ~trust env kn dcl =
           feedback_completion_typecheck feedback_id;
           c, uctx) in
       let def = OpaqueDef (Opaqueproof.create proofterm) in
-      def, RegularArity typ, None, c.const_entry_polymorphic, 
-	c.const_entry_universes,
-	c.const_entry_inline_code, c.const_entry_secctx
+      def, RegularArity typ, None,
+      (Monomorphic_const c.const_entry_universes),
+      c.const_entry_inline_code, c.const_entry_secctx
 
   (** Other definitions have to be processed immediately. *)
   | DefinitionEntry c ->
@@ -279,7 +289,8 @@ let infer_declaration ~trust env kn dcl =
       let env = push_context_set ~strict:(not c.const_entry_polymorphic) ctx env in
       let abstract = c.const_entry_polymorphic && not (Option.is_empty kn) in
       let usubst, univs =
-	Univ.abstract_universes abstract (Univ.ContextSet.to_context ctx) in      
+        abstract_constant_universes abstract (Univ.ContextSet.to_context ctx)
+      in      
       let j = infer env body in
       let typ = match typ with
         | None ->
@@ -298,8 +309,7 @@ let infer_declaration ~trust env kn dcl =
 	else Def (Mod_subst.from_val def) 
       in
 	feedback_completion_typecheck feedback_id;
-	def, typ, None, c.const_entry_polymorphic,
-        univs, c.const_entry_inline_code, c.const_entry_secctx
+	def, typ, None, univs, c.const_entry_inline_code, c.const_entry_secctx
 
   | ProjectionEntry {proj_entry_ind = ind; proj_entry_arg = i} ->
     let mib, _ = Inductive.lookup_mind_specif env (ind,0) in
@@ -311,9 +321,16 @@ let infer_declaration ~trust env kn dcl =
 	else assert false
       | _ -> assert false
     in
+    let univs =
+      match mib.mind_universes with
+      | Monomorphic_ind ctx -> Monomorphic_const ctx
+      | Polymorphic_ind auctx -> Polymorphic_const auctx
+      | Cumulative_ind acumi ->
+        Polymorphic_const (Univ.ACumulativityInfo.univ_context acumi)
+    in
     let term, typ = pb.proj_eta in
       Def (Mod_subst.from_val (hcons_constr term)), RegularArity typ, Some pb,
-      mib.mind_polymorphic, Univ.UInfoInd.univ_context mib.mind_universes, false, None
+      univs, false, None
 
 let global_vars_set_constant_type env = function
   | RegularArity t -> global_vars_set env t
@@ -337,7 +354,7 @@ let record_aux env s_ty s_bo suggested_expr =
 let suggest_proof_using = ref (fun _ _ _ _ _ -> "")
 let set_suggest_proof_using f = suggest_proof_using := f
 
-let build_constant_declaration kn env (def,typ,proj,poly,univs,inline_code,ctx) =
+let build_constant_declaration kn env (def,typ,proj,univs,inline_code,ctx) =
   let check declared inferred =
     let mk_set l = List.fold_right Id.Set.add (List.map NamedDecl.get_id l) Id.Set.empty in
     let inferred_set, declared_set = mk_set inferred, mk_set declared in
@@ -409,9 +426,8 @@ let build_constant_declaration kn env (def,typ,proj,poly,univs,inline_code,ctx)
               check declared inferred) lc) in
   let tps = 
     let res =
-      let comp_univs = if poly then Some univs else None in
       match proj with
-      | None -> compile_constant_body env comp_univs def
+      | None -> compile_constant_body env univs def
       | Some pb ->
 	(* The compilation of primitive projections is a bit tricky, because
            they refer to themselves (the body of p looks like fun c =>
@@ -425,14 +441,13 @@ let build_constant_declaration kn env (def,typ,proj,poly,univs,inline_code,ctx)
 	    const_type = typ;
 	    const_proj = proj;
 	    const_body_code = None;
-	    const_polymorphic = poly;
 	    const_universes = univs;
 	    const_inline_code = inline_code;
 	    const_typing_flags = Environ.typing_flags env;
 	    }
 	in
 	let env = add_constant kn cb env in
-	compile_constant_body env comp_univs def
+	compile_constant_body env univs def
     in Option.map Cemitcodes.from_val res
   in
   { const_hyps = hyps;
@@ -440,7 +455,6 @@ let build_constant_declaration kn env (def,typ,proj,poly,univs,inline_code,ctx)
     const_type = typ;
     const_proj = proj;
     const_body_code = tps;
-    const_polymorphic = poly;
     const_universes = univs;
     const_inline_code = inline_code;
     const_typing_flags = Environ.typing_flags env }
@@ -452,6 +466,12 @@ let translate_constant mb env kn ce =
     (infer_declaration ~trust:mb env (Some kn) ce)
 
 let constant_entry_of_side_effect cb u =
+  let poly, univs =
+    match cb.const_universes with
+    | Monomorphic_const ctx -> false, ctx
+    | Polymorphic_const auctx -> 
+      true, Univ.instantiate_univ_context auctx
+  in
   let pt =
     match cb.const_body, u with
     | OpaqueDef _, `Opaque (b, c) -> b, c
@@ -463,8 +483,8 @@ let constant_entry_of_side_effect cb u =
     const_entry_feedback = None;
     const_entry_type =
       (match cb.const_type with RegularArity t -> Some t | _ -> None);
-    const_entry_polymorphic = cb.const_polymorphic;
-    const_entry_universes = cb.const_universes;
+    const_entry_polymorphic = poly;
+    const_entry_universes = univs;
     const_entry_opaque = Declareops.is_opaque cb;
     const_entry_inline_code = cb.const_inline_code }
 ;;
@@ -508,16 +528,23 @@ let export_side_effects mb env ce =
       let trusted = check_signatures mb signatures in
       let push_seff env = function
         | kn, cb, `Nothing, _ ->
-           let env = Environ.add_constant kn cb env in
-	   if not cb.const_polymorphic then
-	     Environ.push_context ~strict:true cb.const_universes env
-	   else env
-        | kn, cb, `Opaque(_, ctx), _ -> 
-           let env = Environ.add_constant kn cb env in
-	   if not cb.const_polymorphic then
-	     let env = Environ.push_context ~strict:true cb.const_universes env in
-             Environ.push_context_set ~strict:true ctx env
-	   else env in
+          begin
+            let env = Environ.add_constant kn cb env in
+            match cb.const_universes with
+            | Monomorphic_const ctx ->
+              Environ.push_context ~strict:true ctx env
+            | Polymorphic_const _ -> env
+          end
+        | kn, cb, `Opaque(_, ctx), _ ->
+          begin
+            let env = Environ.add_constant kn cb env in
+            match cb.const_universes with
+            | Monomorphic_const cstctx ->
+              let env = Environ.push_context ~strict:true cstctx env in
+              Environ.push_context_set ~strict:true ctx env
+            | Polymorphic_const _ -> env
+          end
+      in
       let rec translate_seff sl seff acc env =
         match sl, seff with
         | _, [] -> List.rev acc, ce
@@ -553,7 +580,7 @@ let translate_recipe env kn r =
   build_constant_declaration kn env (Cooking.cook_constant ~hcons env r)
 
 let translate_local_def mb env id centry =
-  let def,typ,proj,poly,univs,inline_code,ctx =
+  let def,typ,proj,univs,inline_code,ctx =
     infer_declaration ~trust:mb env None (DefinitionEntry centry) in
   let typ = type_of_constant_type env typ in
   if ctx = None && !Flags.compilation_mode = Flags.BuildVo then begin
diff --git a/kernel/typeops.ml b/kernel/typeops.ml
index 1a07bb2fc..e08f3362d 100644
--- a/kernel/typeops.ml
+++ b/kernel/typeops.ml
@@ -555,7 +555,7 @@ let type_of_projection_constant env (p,u) =
   let cb = lookup_constant cst env in
   match cb.const_proj with
   | Some pb ->
-    if cb.const_polymorphic then
+    if Declareops.constant_is_polymorphic cb then
       Vars.subst_instance_constr u pb.proj_type
     else pb.proj_type
   | None -> raise (Invalid_argument "type_of_projection: not a projection")
diff --git a/kernel/univ.ml b/kernel/univ.ml
index eb45f022e..8cbb20a05 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -1031,7 +1031,13 @@ end
 type universe_context = UContext.t
 let hcons_universe_context = UContext.hcons
 
-(** Universe info for inductive types: A context of universe levels
+module AUContext = UContext
+
+type abstract_universe_context = AUContext.t
+let hcons_abstract_universe_context = AUContext.hcons
+
+(** Universe info for cumulative inductive types:
+    A context of universe levels
     with universe constraints, representing local universe variables
     and constraints, together with a context of universe levels with
     universe constraints, representing conditions for subtyping used
@@ -1040,7 +1046,7 @@ let hcons_universe_context = UContext.hcons
     This data structure maintains the invariant that the context for
     subtyping constraints is exactly twice as big as the context for
     universe constraints. *)
-module UInfoInd =
+module CumulativityInfo =
 struct
   type t = universe_context * universe_context
 
@@ -1093,8 +1099,13 @@ struct
 
 end
 
-type universe_info_ind = UInfoInd.t
-let hcons_universe_info_ind = UInfoInd.hcons
+type cumulativity_info = CumulativityInfo.t
+let hcons_cumulativity_info = CumulativityInfo.hcons
+
+module ACumulativityInfo = CumulativityInfo
+
+type abstract_cumulativity_info = ACumulativityInfo.t
+let hcons_abstract_cumulativity_info = ACumulativityInfo.hcons
 
 (** A set of universes with universe constraints.
     We linearize the set to a list after typechecking. 
@@ -1200,6 +1211,9 @@ let subst_univs_level_constraints subst csts =
     (fun c -> Option.fold_right Constraint.add (subst_univs_level_constraint subst c))
     csts Constraint.empty 
 
+let subst_univs_level_abstract_universe_context subst (inst, csts) =
+  inst, subst_univs_level_constraints subst csts
+
 (** With level to universe substitutions. *)
 type universe_subst_fn = universe_level -> universe
 
@@ -1272,12 +1286,9 @@ let instantiate_univ_context (ctx, csts) =
   (ctx, subst_instance_constraints ctx csts)
 
 (** Substitute instance inst for ctx in universe constraints and subtyping constraints *)
-let instantiate_univ_info_ind (univcst, subtpcst) = 
+let instantiate_cumulativity_info (univcst, subtpcst) = 
   (instantiate_univ_context univcst, instantiate_univ_context subtpcst)
 
-let instantiate_univ_constraints u (_, csts) = 
-  subst_instance_constraints u csts
-
 let make_instance_subst i = 
   let arr = Instance.to_array i in
     Array.fold_left_i (fun i acc l ->
@@ -1290,16 +1301,22 @@ let make_inverse_instance_subst i =
       LMap.add (Level.var i) l acc)
       LMap.empty arr
 
-let abstract_universes poly ctx =
+let make_abstract_instance (ctx, _) = 
+  Array.mapi (fun i l -> Level.var i) ctx
+
+let abstract_universes ctx =
   let instance = UContext.instance ctx in
-    if poly then
-      let subst = make_instance_subst instance in
-      let cstrs = subst_univs_level_constraints subst 
-	(UContext.constraints ctx)
-      in
-      let ctx = UContext.make (instance, cstrs) in
-	subst, ctx
-    else empty_level_subst, ctx
+  let subst = make_instance_subst instance in
+  let cstrs = subst_univs_level_constraints subst 
+      (UContext.constraints ctx)
+  in
+  let ctx = UContext.make (instance, cstrs) in
+  subst, ctx
+
+let abstract_cumulativity_info (univcst, substcst) = 
+  let instance, univcst = abstract_universes univcst in
+  let _, substcst = abstract_universes substcst in
+  (instance, (univcst, substcst))
 
 (** Pretty-printing *)
 
@@ -1307,7 +1324,11 @@ let pr_constraints prl = Constraint.pr prl
 
 let pr_universe_context = UContext.pr
 
-let pr_universe_info_ind = UInfoInd.pr
+let pr_cumulativity_info = CumulativityInfo.pr
+
+let pr_abstract_universe_context = AUContext.pr
+
+let pr_abstract_cumulativity_info = ACumulativityInfo.pr
 
 let pr_universe_context_set = ContextSet.pr
 
@@ -1364,3 +1385,12 @@ let subst_instance_constraints =
     let key = Profile.declare_profile "subst_instance_constraints" in
       Profile.profile2 key subst_instance_constraints
   else subst_instance_constraints
+
+let subst_instance_context = 
+  let subst_instance_context_body inst (inner_inst, inner_constr) =
+    (inner_inst, subst_instance_constraints inst inner_constr)
+  in
+  if Flags.profile then 
+    let key = Profile.declare_profile "subst_instance_constraints" in
+      Profile.profile2 key subst_instance_context_body
+  else subst_instance_context_body
diff --git a/kernel/univ.mli b/kernel/univ.mli
index 53af80448..ecc72701d 100644
--- a/kernel/univ.mli
+++ b/kernel/univ.mli
@@ -315,6 +315,23 @@ end
 
 type universe_context = UContext.t
 
+module AUContext :
+sig 
+  type t
+
+  val empty : t
+
+  val instance : t -> Instance.t
+                        
+  val size : t -> int
+
+  (** Keeps the order of the instances *)
+  val union : t -> t -> t
+
+end
+
+type abstract_universe_context = AUContext.t
+
 (** Universe info for inductive types: A context of universe levels
     with universe constraints, representing local universe variables
     and constraints, together with a context of universe levels with
@@ -324,7 +341,7 @@ type universe_context = UContext.t
     This data structure maintains the invariant that the context for
     subtyping constraints is exactly twice as big as the context for
     universe constraints. *)
-module UInfoInd :
+module CumulativityInfo :
 sig
   type t
 
@@ -347,7 +364,17 @@ 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
 
 (** Universe contexts (as sets) *)
 
@@ -399,6 +426,8 @@ val is_empty_level_subst : universe_level_subst -> bool
 val subst_univs_level_level : universe_level_subst -> universe_level -> universe_level
 val subst_univs_level_universe : universe_level_subst -> universe -> universe
 val subst_univs_level_constraints : universe_level_subst -> constraints -> constraints
+val subst_univs_level_abstract_universe_context :
+  universe_level_subst -> abstract_universe_context -> abstract_universe_context
 val subst_univs_level_instance : universe_level_subst -> universe_instance -> universe_instance
 
 (** Level to universe substitutions. *)
@@ -413,27 +442,31 @@ val subst_univs_constraints : universe_subst_fn -> constraints -> constraints
 (** 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
 
-val abstract_universes : bool -> universe_context -> universe_level_subst * universe_context
+val abstract_universes : universe_context -> universe_level_subst * abstract_universe_context
+
+val abstract_cumulativity_info : cumulativity_info -> universe_level_subst * abstract_cumulativity_info
+
+val make_abstract_instance : abstract_universe_context -> universe_instance
 
 (** Get the instantiated graph. *)
-val instantiate_univ_context : universe_context -> universe_context
+val instantiate_univ_context : abstract_universe_context -> universe_context
 
 (** Get the instantiated graphs for both universe constraints and subtyping constraints. *)
-val instantiate_univ_info_ind : universe_info_ind -> universe_info_ind
-
-val instantiate_univ_constraints : universe_instance -> universe_context -> constraints
+val instantiate_cumulativity_info : abstract_cumulativity_info -> cumulativity_info
 
 (** {6 Pretty-printing of universes. } *)
 
 val pr_constraint_type : constraint_type -> Pp.std_ppcmds
 val pr_constraints : (Level.t -> Pp.std_ppcmds) -> constraints -> Pp.std_ppcmds
 val pr_universe_context : (Level.t -> Pp.std_ppcmds) -> universe_context -> Pp.std_ppcmds
-val pr_universe_info_ind : (Level.t -> Pp.std_ppcmds) -> universe_info_ind -> Pp.std_ppcmds
+val pr_cumulativity_info : (Level.t -> Pp.std_ppcmds) -> cumulativity_info -> Pp.std_ppcmds
+val pr_abstract_universe_context : (Level.t -> Pp.std_ppcmds) -> abstract_universe_context -> Pp.std_ppcmds
+val pr_abstract_cumulativity_info : (Level.t -> Pp.std_ppcmds) -> abstract_cumulativity_info -> Pp.std_ppcmds
 val pr_universe_context_set : (Level.t -> Pp.std_ppcmds) -> universe_context_set -> Pp.std_ppcmds
 val explain_universe_inconsistency : (Level.t -> Pp.std_ppcmds) -> 
   univ_inconsistency -> Pp.std_ppcmds
@@ -447,8 +480,10 @@ val hcons_univ : universe -> universe
 val hcons_constraints : constraints -> constraints
 val hcons_universe_set : universe_set -> universe_set
 val hcons_universe_context : universe_context -> universe_context
+val hcons_abstract_universe_context : abstract_universe_context -> abstract_universe_context
 val hcons_universe_context_set : universe_context_set -> universe_context_set 
-val hcons_universe_info_ind : universe_info_ind -> universe_info_ind
+val hcons_cumulativity_info : cumulativity_info -> cumulativity_info
+val hcons_abstract_cumulativity_info : abstract_cumulativity_info -> abstract_cumulativity_info
 
 (******)
 
diff --git a/kernel/vconv.ml b/kernel/vconv.ml
index fa1662270..0e452621c 100644
--- a/kernel/vconv.ml
+++ b/kernel/vconv.ml
@@ -88,30 +88,34 @@ and conv_atom env pb k a1 stk1 a2 stk2 cu =
 (*  Pp.(msg_debug (str "conv_atom(" ++ pr_atom a1 ++ str ", " ++ pr_atom a2 ++ str ")")) ; *)
   match a1, a2 with
   | Aind ((mi,i) as ind1) , Aind ind2 ->
-      if eq_ind ind1 ind2 && compare_stack stk1 stk2
-      then
-        if Environ.polymorphic_ind ind1 env
-        then
-          let mib = Environ.lookup_mind mi env 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' ->
-	     assert (ulen <= nargs args1);
-             assert (ulen <= nargs args2);
-	     let u1 = Array.init ulen (fun i -> uni_lvl_val (arg args1 i)) in
-	     let u2 = Array.init ulen (fun i -> uni_lvl_val (arg args2 i)) in
-	     let u1 = Univ.Instance.of_array u1 in
-	     let u2 = Univ.Instance.of_array u2 in
-	     let cu = convert_instances ~flex:false u1 u2 cu in
-             conv_arguments env ~from:ulen k args1 args2
-			    (conv_stack env k stk1' stk2' cu)
-	  | _, _ -> assert false (* Should not happen if problem is well typed *)
-        else
-	  conv_stack env k stk1 stk2 cu
-      else raise NotConvertible
+    if eq_ind ind1 ind2 && compare_stack stk1 stk2 then
+      if Environ.polymorphic_ind ind1 env then
+        let mib = Environ.lookup_mind mi env in
+	let ulen = 
+          match mib.Declarations.mind_universes with
+          | Declarations.Monomorphic_ind ctx -> Univ.UContext.size ctx
+          | Declarations.Polymorphic_ind auctx -> Univ.AUContext.size auctx
+          | Declarations.Cumulative_ind cumi -> 
+            Univ.AUContext.size (Univ.ACumulativityInfo.univ_context cumi)
+        in
+        match stk1 , stk2 with
+	| [], [] -> assert (Int.equal ulen 0); cu
+        | Zapp args1 :: stk1' , Zapp args2 :: stk2' ->
+          assert (ulen <= nargs args1);
+          assert (ulen <= nargs args2);
+          let u1 = Array.init ulen (fun i -> uni_lvl_val (arg args1 i)) in
+          let u2 = Array.init ulen (fun i -> uni_lvl_val (arg args2 i)) in
+          let u1 = Univ.Instance.of_array u1 in
+          let u2 = Univ.Instance.of_array u2 in
+          let cu = convert_instances ~flex:false u1 u2 cu in
+          conv_arguments env ~from:ulen k args1 args2
+	    (conv_stack env k stk1' stk2' cu)
+        | _, _ -> assert false (* Should not happen if problem is well typed *)
+      else
+	conv_stack env k stk1 stk2 cu
+    else raise NotConvertible
   | Aid ik1, Aid ik2 ->
-      if Vars.eq_id_key ik1 ik2 && compare_stack stk1 stk2 then
+    if Vars.eq_id_key ik1 ik2 && compare_stack stk1 stk2 then
 	conv_stack env k stk1 stk2 cu
       else raise NotConvertible
   | Atype _ , _ | _, Atype _ -> assert false
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.
diff --git a/pretyping/arguments_renaming.ml b/pretyping/arguments_renaming.ml
index 1bd03491a..c7b37aba5 100644
--- a/pretyping/arguments_renaming.ml
+++ b/pretyping/arguments_renaming.ml
@@ -43,7 +43,7 @@ let section_segment_of_reference = function
   | ConstRef con -> Lib.section_segment_of_constant con
   | IndRef (kn,_) | ConstructRef ((kn,_),_) ->
       Lib.section_segment_of_mutual_inductive kn
-  | _ -> [], Univ.LMap.empty, Univ.UContext.empty
+  | _ -> [], Univ.LMap.empty, Univ.AUContext.empty
 
 let discharge_rename_args = function
   | _, (ReqGlobal (c, names), _ as req) ->
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index be2fd8129..b15dde5d7 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -350,18 +350,22 @@ let exact_ise_stack2 env evd f sk1 sk2 =
     ise_stack2 evd (List.rev sk1) (List.rev sk2)
   else UnifFailure (evd, (* Dummy *) NotSameHead)
 
-let check_leq_inductives evd uinfind u u' =
+let check_leq_inductives evd cumi u u' =
   let u = EConstr.EInstance.kind evd u in
   let u' = EConstr.EInstance.kind evd u' in
-  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 ind_instance = 
+    Univ.AUContext.instance (Univ.ACumulativityInfo.univ_context cumi) 
+  in
+  let ind_sbcst =  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!")
   else
     begin
      let comp_subst = (Univ.Instance.append u u') in
-     let comp_cst = Univ.subst_instance_constraints comp_subst ind_sbcst in
+     let comp_cst = 
+       Univ.UContext.constraints (Univ.subst_instance_context comp_subst ind_sbcst)
+     in
      Evd.add_constraints evd comp_cst
     end
 
@@ -491,23 +495,24 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
           let nparamsaplied' = Stack.args_size sk' in
           begin
             let mind = Environ.lookup_mind (fst ind) env in
-            if mind.Declarations.mind_polymorphic then
+            match mind.Declarations.mind_universes with
+            | Declarations.Monomorphic_ind _ | Declarations.Polymorphic_ind _ ->
+              UnifFailure (evd, NotSameHead)
+            | Declarations.Cumulative_ind cumi ->
               begin
                 let num_param_arity =
-                  (* Context.Rel.length (mind.Declarations.mind_packets.(snd ind).Declarations.mind_arity_ctxt) *)
-                  mind.Declarations.mind_nparams + mind.Declarations.mind_packets.(snd ind).Declarations.mind_nrealargs
+                  mind.Declarations.mind_nparams + 
+                  mind.Declarations.mind_packets.(snd ind).Declarations.mind_nrealargs
                 in
-                if not (num_param_arity = nparamsaplied && num_param_arity = nparamsaplied') then
+                if not (num_param_arity = nparamsaplied
+                        && num_param_arity = nparamsaplied') then
                   UnifFailure (evd, NotSameHead)
                 else
                   begin
-                    let uinfind = mind.Declarations.mind_universes in
-                    let evd' = check_leq_inductives evd uinfind u u' in
-                    Success (check_leq_inductives evd' uinfind u' u)
+                    let evd' = check_leq_inductives evd cumi u u' in
+                    Success (check_leq_inductives evd' cumi u' u)
                   end
               end
-            else
-              UnifFailure (evd, NotSameHead)
           end
         in
         first_try_strict_check (Names.eq_ind ind ind') u u' check_subtyping_constraints
@@ -518,26 +523,29 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
           let nparamsaplied = Stack.args_size sk in
           let nparamsaplied' = Stack.args_size sk' in
           let mind = Environ.lookup_mind (fst ind) env in
-          if mind.Declarations.mind_polymorphic then
+          match mind.Declarations.mind_universes with
+          | Declarations.Monomorphic_ind _ | Declarations.Polymorphic_ind _ ->
+            UnifFailure (evd, NotSameHead)
+          | Declarations.Cumulative_ind cumi ->
             begin
               let num_cnstr_args =
                 let nparamsctxt =
-                  (* Context.Rel.length mind.Declarations.mind_params_ctxt *)
-                  mind.Declarations.mind_nparams + mind.Declarations.mind_packets.(snd ind).Declarations.mind_nrealargs
+                  mind.Declarations.mind_nparams + 
+                  mind.Declarations.mind_packets.(snd ind).Declarations.mind_nrealargs
                 in
-                nparamsctxt + mind.Declarations.mind_packets.(snd ind).Declarations.mind_consnrealargs.(j - 1)
+                nparamsctxt + 
+                mind.Declarations.mind_packets.(snd ind).
+                  Declarations.mind_consnrealargs.(j - 1)
               in
-              if not (num_cnstr_args = nparamsaplied && num_cnstr_args = nparamsaplied') then
+              if not (num_cnstr_args = nparamsaplied 
+                      && num_cnstr_args = nparamsaplied') then
                 UnifFailure (evd, NotSameHead)
               else
                 begin
-                  let uinfind = mind.Declarations.mind_universes in
-                  let evd' = check_leq_inductives evd uinfind u u' in
-                  Success (check_leq_inductives evd' uinfind u' u)
+                  let evd' = check_leq_inductives evd cumi u u' in
+                  Success (check_leq_inductives evd' cumi u' u)
                 end
             end
-          else
-            UnifFailure (evd, NotSameHead)
         in
         first_try_strict_check (Names.eq_constructor cons cons') u u' check_subtyping_constraints
       | _, _ -> anomaly (Pp.str "")
@@ -546,7 +554,6 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
                 try compare_heads i
                 with Univ.UniverseInconsistency p -> UnifFailure (i, UnifUnivInconsistency p));
                  (fun i -> exact_ise_stack2 env i (evar_conv_x ts) sk sk')]
-(* >>>>>>> Make unification use subtyping info of inductives *)
   in
   let flex_maybeflex on_left ev ((termF,skF as apprF),cstsF) ((termM, skM as apprM),cstsM) vM =
     let switch f a b = if on_left then f a b else f b a in
diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml
index 1ef4a9f5e..2ae7c0f80 100644
--- a/pretyping/inductiveops.ml
+++ b/pretyping/inductiveops.ml
@@ -696,39 +696,52 @@ let infer_inductive_subtyping_arity_constructor
 let infer_inductive_subtyping env evd mind_ent =
   let { Entries.mind_entry_params = params;
         Entries.mind_entry_inds = entries;
-        Entries.mind_entry_polymorphic = poly;
-        Entries.mind_entry_cumulative = cum;
-        Entries.mind_entry_universes = ground_uinfind;
+        Entries.mind_entry_universes = ground_univs;
       } = mind_ent
   in
   let uinfind =
-    if poly && cum then
-    begin
-      let uctx = Univ.UInfoInd.univ_context ground_uinfind in
-      let sbsubst = Univ.UInfoInd.subtyping_susbst ground_uinfind in
-      let dosubst = subst_univs_level_constr sbsubst in
-      let instance_other = Univ.subst_univs_level_instance sbsubst (Univ.UContext.instance uctx) in
-      let constraints_other = Univ.subst_univs_level_constraints sbsubst (Univ.UContext.constraints uctx) in
-      let uctx_other = Univ.UContext.make (instance_other, constraints_other) in
-      let env = Environ.push_context uctx env in
-      let env = Environ.push_context uctx_other env in
-      let evd = Evd.merge_universe_context evd (UState.of_context_set (Univ.ContextSet.of_context uctx_other)) in
-      let (_, _, subtyp_constraints) =
-        List.fold_left
-          (fun ctxs indentry ->
-             let _, params = Typeops.infer_local_decls env params in
-             let ctxs' = infer_inductive_subtyping_arity_constructor
-                 ctxs dosubst indentry.Entries.mind_entry_arity true params
-             in
-             List.fold_left
-               (fun ctxs cons ->
-                  infer_inductive_subtyping_arity_constructor ctxs dosubst cons false params)
-               ctxs' indentry.Entries.mind_entry_lc
-          ) (env, evd, Univ.Constraint.empty) entries
-      in Univ.UInfoInd.make (Univ.UInfoInd.univ_context ground_uinfind,
-           Univ.UContext.make
-             (Univ.UContext.instance (Univ.UInfoInd.subtyp_context ground_uinfind),
-               subtyp_constraints))
-    end
-    else ground_uinfind
+    match ground_univs with
+    | Entries.Monomorphic_ind_entry _
+    | Entries.Polymorphic_ind_entry _ -> ground_univs
+    | Entries.Cumulative_ind_entry cumi -> 
+      begin
+        let uctx = Univ.CumulativityInfo.univ_context cumi in
+        let sbsubst = Univ.CumulativityInfo.subtyping_susbst cumi in
+        let dosubst = subst_univs_level_constr sbsubst in
+        let instance_other = 
+          Univ.subst_univs_level_instance sbsubst (Univ.UContext.instance uctx) 
+        in
+        let constraints_other = 
+          Univ.subst_univs_level_constraints
+            sbsubst (Univ.UContext.constraints uctx) 
+        in
+        let uctx_other = Univ.UContext.make (instance_other, constraints_other) in
+        let env = Environ.push_context uctx env in
+        let env = Environ.push_context uctx_other env in
+        let evd = 
+          Evd.merge_universe_context
+            evd (UState.of_context_set (Univ.ContextSet.of_context uctx_other)) 
+        in
+        let (_, _, subtyp_constraints) =
+          List.fold_left
+            (fun ctxs indentry ->
+               let _, params = Typeops.infer_local_decls env params in
+               let ctxs' = infer_inductive_subtyping_arity_constructor
+                   ctxs dosubst indentry.Entries.mind_entry_arity true params
+               in
+               List.fold_left
+                 (fun ctxs cons ->
+                    infer_inductive_subtyping_arity_constructor
+                      ctxs dosubst cons false params
+                 )
+                 ctxs' indentry.Entries.mind_entry_lc
+            ) (env, evd, Univ.Constraint.empty) entries
+        in 
+        Entries.Cumulative_ind_entry
+          (Univ.CumulativityInfo.make 
+             (Univ.CumulativityInfo.univ_context cumi,
+              Univ.UContext.make
+                (Univ.UContext.instance (Univ.CumulativityInfo.subtyp_context cumi),
+                 subtyp_constraints)))
+      end
   in {mind_ent with Entries.mind_entry_universes = uinfind;}
diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml
index bc9e3a1f4..283a1dcd1 100644
--- a/pretyping/recordops.ml
+++ b/pretyping/recordops.ml
@@ -197,7 +197,7 @@ let warn_projection_no_head_constant =
 (* Intended to always succeed *)
 let compute_canonical_projections warn (con,ind) =
   let env = Global.env () in
-  let ctx = Univ.instantiate_univ_context (Environ.constant_context env con) in
+  let ctx = Environ.constant_context env con in
   let u = Univ.UContext.instance ctx in
   let v = (mkConstU (con,u)) in
   let ctx = Univ.ContextSet.of_context ctx in
@@ -298,8 +298,7 @@ let error_not_structure ref =
 let check_and_decompose_canonical_structure ref =
   let sp = match ref with ConstRef sp -> sp | _ -> error_not_structure ref in
   let env = Global.env () in
-  let ctx = Environ.constant_context env sp in
-  let u = Univ.UContext.instance ctx in
+  let u = Environ.constant_instance env sp in
   let vc = match Environ.constant_opt_value_in env (sp, u) with
     | Some vc -> vc
     | None -> error_not_structure ref in
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index 2040acba7..123c61016 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -1362,21 +1362,25 @@ let sigma_compare_instances ~flex i0 i1 sigma =
 	raise Reduction.NotConvertible
 
 let sigma_check_inductive_instances cv_pb uinfind u u' sigma =
-  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 ind_instance = 
+    Univ.AUContext.instance (Univ.ACumulativityInfo.univ_context uinfind) 
+  in
+  let ind_sbctx =  Univ.ACumulativityInfo.subtyp_context uinfind  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!")
   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_sbctx)
     in
     let comp_cst =
       match cv_pb with
         Reduction.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' = 
+          Univ.UContext.constraints(Univ.subst_instance_context comp_subst ind_sbctx)
+        in
         Univ.Constraint.union comp_cst comp_cst'
       | Reduction.CUMUL -> comp_cst
     in
@@ -1389,34 +1393,43 @@ let sigma_conv_inductives
     cv_pb (mind, ind) u1 sv1 u2 sv2 sigma =
   try sigma_compare_instances ~flex:false u1 u2 sigma with
     Reduction.NotConvertible ->
-    if mind.Declarations.mind_polymorphic then
+    match mind.Declarations.mind_universes with
+    | Declarations.Monomorphic_ind _ ->
+      raise Reduction.NotConvertible
+    | Declarations.Polymorphic_ind _ ->
+      raise Reduction.NotConvertible
+    | Declarations.Cumulative_ind cumi ->
       let num_param_arity =
-        mind.Declarations.mind_nparams + mind.Declarations.mind_packets.(ind).Declarations.mind_nrealargs
+        mind.Declarations.mind_nparams + 
+        mind.Declarations.mind_packets.(ind).Declarations.mind_nrealargs
       in
       if not (num_param_arity = sv1 && num_param_arity = sv2) then
         raise Reduction.NotConvertible
       else
-        let uinfind = mind.Declarations.mind_universes in
-        sigma_check_inductive_instances cv_pb uinfind u1 u2 sigma
-    else raise Reduction.NotConvertible
+        sigma_check_inductive_instances cv_pb cumi u1 u2 sigma 
 
 let sigma_conv_constructors
     (mind, ind, cns) u1 sv1 u2 sv2 sigma =
   try sigma_compare_instances ~flex:false u1 u2 sigma with
     Reduction.NotConvertible ->
-    if mind.Declarations.mind_polymorphic then
+    match mind.Declarations.mind_universes with
+    | Declarations.Monomorphic_ind _ ->
+      raise Reduction.NotConvertible
+    | Declarations.Polymorphic_ind _ ->
+      raise Reduction.NotConvertible
+    | Declarations.Cumulative_ind cumi ->
       let num_cnstr_args =
         let nparamsctxt =
-          mind.Declarations.mind_nparams + mind.Declarations.mind_packets.(ind).Declarations.mind_nrealargs
-          (* Context.Rel.length mind.Declarations.mind_params_ctxt *) in
-        nparamsctxt + mind.Declarations.mind_packets.(ind).Declarations.mind_consnrealargs.(cns - 1)
+          mind.Declarations.mind_nparams + 
+          mind.Declarations.mind_packets.(ind).Declarations.mind_nrealargs
+        in
+        nparamsctxt + 
+        mind.Declarations.mind_packets.(ind).Declarations.mind_consnrealargs.(cns - 1)
       in
       if not (num_cnstr_args = sv1 && num_cnstr_args = sv2) then
         raise Reduction.NotConvertible
       else
-        let uinfind = mind.Declarations.mind_universes in
-        sigma_check_inductive_instances Reduction.CONV uinfind u1 u2 sigma
-    else raise Reduction.NotConvertible
+        sigma_check_inductive_instances Reduction.CONV cumi u1 u2 sigma
 
 let sigma_univ_state = 
   { Reduction.compare = sigma_compare_sorts;
diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml
index 152ccb079..f883e647b 100644
--- a/pretyping/typeclasses.ml
+++ b/pretyping/typeclasses.ml
@@ -111,20 +111,16 @@ let new_instance cl info glob poly impl =
 let classes : typeclasses ref = Summary.ref Refmap.empty ~name:"classes"
 let instances : instances ref = Summary.ref Refmap.empty ~name:"instances"
 
-open Declarations
-
 let typeclass_univ_instance (cl,u') =
   let subst = 
     let u = 
       match cl.cl_impl with
       | ConstRef c -> 
         let cb = Global.lookup_constant c in
-	  if cb.const_polymorphic then Univ.UContext.instance cb.const_universes
-	  else Univ.Instance.empty
+        Declareops.constant_polymorphic_instance cb
       | IndRef c ->
          let mib,oib = Global.lookup_inductive c in
-	  if mib.mind_polymorphic then Univ.UContext.instance (Univ.UInfoInd.univ_context mib.mind_universes)
-	  else Univ.Instance.empty
+         Declareops.inductive_polymorphic_instance mib
       | _ -> Univ.Instance.empty
     in Array.fold_left2 (fun subst u u' -> Univ.LMap.add u u' subst) 
       Univ.LMap.empty (Univ.Instance.to_array u) (Univ.Instance.to_array u')
diff --git a/pretyping/vnorm.ml b/pretyping/vnorm.ml
index 074b7373c..9e151fea2 100644
--- a/pretyping/vnorm.ml
+++ b/pretyping/vnorm.ml
@@ -174,8 +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 (Univ.UInfoInd.univ_context mib.mind_universes)
-       else 0
+       Univ.Instance.length (Declareops.inductive_polymorphic_instance mib)
      in
      let mk u =
        let pind = (ind, u) in (mkIndU pind, type_of_ind env pind)
@@ -204,8 +203,7 @@ and constr_type_of_idkey env sigma (idkey : Vars.id_key) stk =
   | ConstKey cst ->
      let cbody = Environ.lookup_constant cst env in
      let nb_univs =
-       if cbody.const_polymorphic then Univ.UContext.size cbody.const_universes
-       else 0
+       Univ.Instance.length (Declareops.constant_polymorphic_instance cbody)
      in
      let mk u =
        let pcst = (cst, u) in (mkConstU pcst, Typeops.type_of_constant_in env pcst)
diff --git a/printing/prettyp.ml b/printing/prettyp.ml
index 3ae7da8fc..6d2bf6b73 100644
--- a/printing/prettyp.ml
+++ b/printing/prettyp.ml
@@ -502,8 +502,8 @@ let ungeneralized_type_of_constant_type t =
   Typeops.type_of_constant_type (Global.env ()) t
 
 let print_instance sigma cb =
-  if cb.const_polymorphic then
-    pr_universe_instance sigma cb.const_universes
+  if Declareops.constant_is_polymorphic cb then
+    pr_universe_instance sigma (Declareops.constant_polymorphic_context cb)
   else mt()
 				
 let print_constant with_values sep sp =
@@ -511,16 +511,14 @@ let print_constant with_values sep sp =
   let val_0 = Global.body_of_constant_body cb in
   let typ = Declareops.type_of_constant cb in
   let typ = ungeneralized_type_of_constant_type typ in
-  let univs = Univ.instantiate_univ_context 
-    (Global.universes_of_constant_body cb)
-  in
+  let univs = Global.universes_of_constant_body cb in
   let ctx =
     Evd.evar_universe_context_of_binders
       (Universes.universe_binders_of_global (ConstRef sp))
   in
   let env = Global.env () and sigma = Evd.from_ctx ctx in
   let pr_ltype = pr_ltype_env env sigma in
-  hov 0 (pr_polymorphic cb.const_polymorphic ++
+  hov 0 (pr_polymorphic (Declareops.constant_is_polymorphic cb) ++
     match val_0 with
     | None ->
 	str"*** [ " ++
diff --git a/printing/printer.ml b/printing/printer.ml
index 1d7b7cff0..3b0b6d5d2 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -261,10 +261,11 @@ 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
+let pr_cumulativity_info sigma cumi =
+  if !Detyping.print_universes 
+  && not (Univ.UContext.is_empty (Univ.CumulativityInfo.univ_context cumi)) then
+    fnl()++pr_in_comment (fun uii -> v 0 
+      (Univ.pr_cumulativity_info (Termops.pr_evd_level sigma) uii)) cumi
   else
     mt()
 
@@ -998,10 +999,10 @@ let pr_assumptionset env s =
 let xor a b = 
   (a && not b) || (not a && b)
 
-let pr_cumulative p b =
-  if p then
-    if b then str "Cumulative " else str "NonCumulative "
-  else str ""
+let pr_cumulative poly cum =
+  if poly then
+    if cum then str "Cumulative " else str "NonCumulative "
+  else mt ()
 
 let pr_polymorphic b = 
   let print = xor (Flags.is_universe_polymorphism ()) b in
diff --git a/printing/printer.mli b/printing/printer.mli
index 9f4ea23b7..f0a32bbbd 100644
--- a/printing/printer.mli
+++ b/printing/printer.mli
@@ -98,7 +98,7 @@ val pr_polymorphic         : bool -> std_ppcmds
 val pr_cumulative          : bool -> 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
+val pr_cumulativity_info   : evar_map -> Univ.cumulativity_info -> std_ppcmds
 
 (** Printing global references using names as short as possible *)
 
diff --git a/printing/printmod.ml b/printing/printmod.ml
index be8940b6f..08d177f53 100644
--- a/printing/printmod.ml
+++ b/printing/printmod.ml
@@ -88,8 +88,8 @@ let build_ind_type env mip =
   Inductive.type_of_inductive env mip
 
 let print_one_inductive env sigma mib ((_,i) as ind) =
-  let u = if mib.mind_polymorphic then 
-      Univ.UContext.instance (Univ.UInfoInd.univ_context mib.mind_universes)
+  let u = if Declareops.inductive_is_polymorphic mib then 
+      Declareops.inductive_polymorphic_instance mib
     else Univ.Instance.empty in
   let mip = mib.mind_packets.(i) in
   let params = Inductive.inductive_paramdecls (mib,u) in
@@ -99,8 +99,8 @@ let print_one_inductive env sigma mib ((_,i) as ind) =
   let cstrtypes = Array.map (fun c -> hnf_prod_applist env c args) cstrtypes in
   let envpar = push_rel_context params env in
   let inst =
-    if mib.mind_polymorphic then
-      Printer.pr_universe_instance sigma (Univ.UInfoInd.univ_context mib.mind_universes)
+    if Declareops.inductive_is_polymorphic mib then
+      Printer.pr_universe_instance sigma (Declareops.inductive_polymorphic_context mib)
     else mt ()
   in
   hov 0 (
@@ -120,12 +120,18 @@ let print_mutual_inductive env mind mib =
   in
   let bl = Universes.universe_binders_of_global (IndRef (mind, 0)) in
   let sigma = Evd.from_ctx (Evd.evar_universe_context_of_binders bl) in
-  hov 0 (Printer.pr_polymorphic mib.mind_polymorphic ++
-         Printer.pr_cumulative mib.mind_polymorphic mib.mind_cumulative ++
+  hov 0 (Printer.pr_polymorphic (Declareops.inductive_is_polymorphic mib) ++
+         Printer.pr_cumulative
+           (Declareops.inductive_is_polymorphic mib) 
+           (Declareops.inductive_is_cumulative mib) ++
          def keyword ++ spc () ++
          prlist_with_sep (fun () -> fnl () ++ str"  with ")
            (print_one_inductive env sigma mib) inds ++
-         Printer.pr_universe_info_ind sigma (Univ.instantiate_univ_info_ind mib.mind_universes))
+         match mib.mind_universes with
+         | Monomorphic_ind _ | Polymorphic_ind _ -> str ""
+         | Cumulative_ind cumi ->
+           Printer.pr_cumulativity_info
+             sigma (Univ.instantiate_cumulativity_info cumi))
 
 let get_fields =
   let rec prodec_rec l subst c =
@@ -142,8 +148,8 @@ let get_fields =
 
 let print_record env mind mib =
   let u = 
-    if mib.mind_polymorphic then 
-      Univ.UContext.instance (Univ.UInfoInd.univ_context mib.mind_universes)
+    if Declareops.inductive_is_polymorphic mib then 
+      Declareops.inductive_polymorphic_instance mib
     else Univ.Instance.empty 
   in
   let mip = mib.mind_packets.(0) in
@@ -165,8 +171,10 @@ let print_record env mind mib =
   in
   hov 0 (
     hov 0 (
-      Printer.pr_polymorphic mib.mind_polymorphic ++
-      Printer.pr_cumulative mib.mind_polymorphic mib.mind_cumulative ++
+      Printer.pr_polymorphic (Declareops.inductive_is_polymorphic mib) ++
+      Printer.pr_cumulative
+        (Declareops.inductive_is_polymorphic mib)
+        (Declareops.inductive_is_cumulative mib) ++
       def keyword ++ spc () ++ pr_id mip.mind_typename ++ brk(1,4) ++
       print_params env sigma params ++
       str ": " ++ Printer.pr_lconstr_env envpar sigma arity ++ brk(1,2) ++
@@ -177,7 +185,12 @@ 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_info_ind sigma (Univ.instantiate_univ_info_ind mib.mind_universes))
+    match mib.mind_universes with
+    | Monomorphic_ind _ | Polymorphic_ind _ -> str ""
+    | Cumulative_ind cumi ->
+      Printer.pr_cumulativity_info
+        sigma (Univ.instantiate_cumulativity_info cumi)
+  )
 
 let pr_mutual_inductive_body env mind mib =
   if mib.mind_record <> None && not !Flags.raw_print then
@@ -280,7 +293,8 @@ let print_body is_impl env mp (l,body) =
     | SFBmodtype _ -> keyword "Module Type" ++ spc () ++ name
     | SFBconst cb ->
        let u =
-	 if cb.const_polymorphic then Univ.UContext.instance cb.const_universes
+	 if Declareops.constant_is_polymorphic cb then
+            Declareops.constant_polymorphic_instance cb
 	 else Univ.Instance.empty
        in
        let sigma = Evd.empty in
@@ -302,7 +316,8 @@ let print_body is_impl env mp (l,body) =
 		       Printer.pr_lconstr_env env sigma
 			  (Vars.subst_instance_constr u (Mod_subst.force_constr l)))
 	      | _ -> mt ()) ++ str "." ++
-	    Printer.pr_universe_ctx sigma (Univ.instantiate_univ_context cb.const_universes))
+	    Printer.pr_universe_ctx sigma 
+              (Declareops.constant_polymorphic_context cb))
     | SFBmind mib ->
       try
 	let env = Option.get env in
diff --git a/tactics/elimschemes.ml b/tactics/elimschemes.ml
index 8d8e19811..99761437e 100644
--- a/tactics/elimschemes.ml
+++ b/tactics/elimschemes.ml
@@ -47,7 +47,7 @@ let optimize_non_type_induction_scheme kind dep sort _ ind =
       (nf c', Evd.evar_universe_context sigma), eff
   else
     let mib,mip = Inductive.lookup_mind_specif env ind in
-    let ctx = Declareops.inductive_context mib in
+    let ctx = Declareops.inductive_polymorphic_context mib in
     let u = Univ.UContext.instance ctx in
     let ctxset = Univ.ContextSet.of_context ctx in
     let ectx = Evd.evar_universe_context_of ctxset in
@@ -60,7 +60,7 @@ let build_induction_scheme_in_type dep sort ind =
   let sigma = Evd.from_env env in
   let ctx = 
     let mib,mip = Inductive.lookup_mind_specif env ind in
-      Declareops.inductive_context mib
+      Declareops.inductive_polymorphic_context mib
   in
   let u = Univ.UContext.instance ctx in
   let ctxset = Univ.ContextSet.of_context ctx in
diff --git a/tactics/elimschemes.mli b/tactics/elimschemes.mli
index 77f927f2d..da432bead 100644
--- a/tactics/elimschemes.mli
+++ b/tactics/elimschemes.mli
@@ -10,6 +10,14 @@ open Ind_tables
 
 (** Induction/recursion schemes *)
 
+val optimize_non_type_induction_scheme : 
+  'a Ind_tables.scheme_kind ->
+  Indrec.dep_flag ->
+  Term.sorts_family ->
+  'b ->
+  Names.inductive ->
+  (Constr.constr * Evd.evar_universe_context) * Safe_typing.private_constants
+
 val rect_scheme_kind_from_prop : individual scheme_kind
 val ind_scheme_kind_from_prop : individual scheme_kind
 val rec_scheme_kind_from_prop : individual scheme_kind
diff --git a/tactics/hints.ml b/tactics/hints.ml
index 681db5d08..2fc8baa89 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -1306,7 +1306,8 @@ let interp_hints poly =
           List.init (nconstructors ind) 
 	    (fun i -> let c = (ind,i+1) in
 		      let gr = ConstructRef c in
-			empty_hint_info, mib.Declarations.mind_polymorphic, true,
+			empty_hint_info, 
+                        (Declareops.inductive_is_polymorphic mib), true,
 			PathHints [gr], IsGlobRef gr)
       in HintsResolveEntry (List.flatten (List.map constr_hints_of_ind lqid))
   | HintsExtern (pri, patcom, tacexp) ->
diff --git a/test-suite/coqchk/cumulativity.v b/test-suite/coqchk/cumulativity.v
index 84121ea92..a978f6b90 100644
--- a/test-suite/coqchk/cumulativity.v
+++ b/test-suite/coqchk/cumulativity.v
@@ -27,14 +27,13 @@ End ListLower.
 
 Lemma LowerL_Lem@{i j} (A : Type@{j}) (l : List@{i} A) : l = LowerL l.
 Proof. reflexivity. Qed.
-
-(* I disable these tests because cqochk can't process them when compiled with
+(*
+I disable these tests because cqochk can't process them when compiled with
    ocaml-4.02.3+32bit and camlp5-4.16 which is the case for Travis!
 
    I have added this file (including the commented parts below) in
    test-suite/success/cumulativity.v which doesn't run coqchk on them.
 *)
-
 (* Inductive Tp := tp : Type -> Tp. *)
 
 (* Section TpLift. *)
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