Merge remote-tracking branch 'upstream/trunk' into trunk

20 files changed, 468 insertions, 84 deletions

diff --git a/checker/cic.mli b/checker/cic.mli
index 3645587554..e298c41cf1 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 abstract_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,9 +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_universes : Univ.universe_context; (** Local universe variables and constraints *)
+    mind_universes : abstract_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/closure.ml b/checker/closure.ml
index b8294e7958..ac8388f6ed 100644
--- a/checker/closure.ml
+++ b/checker/closure.ml
@@ -328,6 +328,12 @@ let zshift n s =
     | (_,Zshift(k)::s) -> Zshift(n+k)::s
     | _ -> Zshift(n)::s
 
+let rec stack_args_size = function
+  | Zapp v :: s -> Array.length v + stack_args_size s
+  | Zshift(_)::s -> stack_args_size s
+  | Zupdate(_)::s -> stack_args_size s
+  | _ -> 0
+
 (* Lifting. Preserves sharing (useful only for cell with norm=Red).
    lft_fconstr always create a new cell, while lift_fconstr avoids it
    when the lift is 0. *)
diff --git a/checker/closure.mli b/checker/closure.mli
index 8b1f246c28..8da9ad4ea5 100644
--- a/checker/closure.mli
+++ b/checker/closure.mli
@@ -125,6 +125,9 @@ type stack_member =
 and stack = stack_member list
 
 val append_stack : fconstr array -> stack -> stack
+
+val stack_args_size : stack -> int
+    
 val eta_expand_stack : stack -> stack
  
 val eta_expand_ind_stack : env -> inductive -> fconstr -> stack -> 
diff --git a/checker/declarations.ml b/checker/declarations.ml
index ad93146d55..2eefe47816 100644
--- a/checker/declarations.ml
+++ b/checker/declarations.ml
@@ -521,6 +521,11 @@ let subst_template_cst_arity sub (ctx,s as arity) =
 
 let subst_arity sub s = subst_decl_arity subst_mps subst_template_cst_arity sub s
 
+let constant_is_polymorphic cb =
+  match cb.const_universes with
+  | Monomorphic_const _ -> false
+  | Polymorphic_const _ -> true
+
 (* TODO: should be changed to non-coping after Term.subst_mps *)
 (* NB: we leave bytecode and native code fields untouched *)
 let subst_const_body sub cb =
diff --git a/checker/declarations.mli b/checker/declarations.mli
index 456df83699..6fc71bb942 100644
--- a/checker/declarations.mli
+++ b/checker/declarations.mli
@@ -14,6 +14,7 @@ val body_of_constant : constant_body -> constr option
 val constant_has_body : constant_body -> bool
 val is_opaque : constant_body -> bool
 val opaque_univ_context : constant_body -> Univ.ContextSet.t
+val constant_is_polymorphic : constant_body -> bool
 
 (* Mutual inductives *)
 
diff --git a/checker/environ.ml b/checker/environ.ml
index 22d1eec178..11b8ea67cc 100644
--- a/checker/environ.ml
+++ b/checker/environ.ml
@@ -115,13 +115,15 @@ let add_constant kn cs env =
 	env_constants = new_constants } in
   { env with env_globals = new_globals }
 
-type const_evaluation_result = NoBody | Opaque
+type const_evaluation_result = NoBody | Opaque | IsProj
 
 (* Constant types *)
 
 let constraints_of cb u =
-  let univs = cb.const_universes in
-    Univ.subst_instance_constraints u (Univ.UContext.constraints univs)
+  match cb.const_universes with
+  | Monomorphic_const _ -> Univ.Constraint.empty
+  | Polymorphic_const ctx -> 
+    Univ.UContext.constraints (Univ.subst_instance_context u ctx)
 
 let map_regular_arity f = function
   | RegularArity a as ar -> 
@@ -132,23 +134,28 @@ let map_regular_arity f = function
 (* constant_type gives the type of a constant *)
 let constant_type env (kn,u) =
   let cb = lookup_constant kn env in
-    if cb.const_polymorphic then
-      let csts = constraints_of cb u in
-	(map_regular_arity (subst_instance_constr u) cb.const_type, csts)
-    else cb.const_type, Univ.Constraint.empty
+  match cb.const_universes with
+  | Monomorphic_const _ -> cb.const_type, Univ.Constraint.empty
+  | Polymorphic_const ctx -> 
+    let csts = constraints_of cb u in
+    (map_regular_arity (subst_instance_constr u) cb.const_type, csts)
 
 exception NotEvaluableConst of const_evaluation_result
 
 let constant_value env (kn,u) =
   let cb = lookup_constant kn env in
+  if cb.const_proj = None then
     match cb.const_body with
     | Def l_body -> 
       let b = force_constr l_body in
-	if cb.const_polymorphic then
-	  subst_instance_constr u (force_constr l_body)
-	else b
+      begin
+        match cb.const_universes with
+        | Monomorphic_const _ -> b
+        | Polymorphic_const _ -> subst_instance_constr u (force_constr l_body)
+      end
     | OpaqueDef _ -> raise (NotEvaluableConst Opaque)
     | Undef _ -> raise (NotEvaluableConst NoBody)
+  else raise (NotEvaluableConst IsProj)
 
 (* A global const is evaluable if it is defined and not opaque *)
 let evaluable_constant cst env =
diff --git a/checker/environ.mli b/checker/environ.mli
index 87f143d1bb..754c295d27 100644
--- a/checker/environ.mli
+++ b/checker/environ.mli
@@ -47,7 +47,7 @@ val check_constraints : Univ.constraints -> env -> bool
 val lookup_constant : constant -> env -> Cic.constant_body
 val add_constant : constant -> Cic.constant_body -> env -> env
 val constant_type : env -> constant puniverses -> constant_type Univ.constrained
-type const_evaluation_result = NoBody | Opaque
+type const_evaluation_result = NoBody | Opaque | IsProj
 exception NotEvaluableConst of const_evaluation_result
 val constant_value : env -> constant puniverses -> constr
 val evaluable_constant : constant -> env -> bool
diff --git a/checker/indtypes.ml b/checker/indtypes.ml
index 6c38f38e29..54dec56b54 100644
--- a/checker/indtypes.ml
+++ b/checker/indtypes.ml
@@ -524,13 +524,67 @@ let check_positivity env_ar mind params nrecp inds =
   let wfp = Rtree.mk_rec irecargs in
   Array.iter2 (fun ind wfpi -> check_subtree ind.mind_recargs wfpi) inds wfp
 
+(* Check arities and constructors *)
+let check_subtyping_arity_constructor env (subst : constr -> constr) (arcn : constr) numparams is_arity =
+  let numchecked = ref 0 in
+  let basic_check ev tp =
+    if !numchecked < numparams then () else conv_leq ev tp (subst tp);
+    numchecked := !numchecked + 1
+  in
+  let check_typ typ typ_env =
+    match typ with
+    | LocalAssum (_, typ') ->
+      begin
+       try
+          basic_check typ_env typ'; Environ.push_rel typ typ_env
+        with NotConvertible -> 
+          anomaly ~label:"bad inductive subtyping relation" (Pp.str "Invalid subtyping relation")
+      end
+    | _ -> anomaly (Pp.str "")
+  in
+  let typs, codom = dest_prod env arcn in
+  let last_env = fold_rel_context_outside check_typ typs ~init:env in
+  if not is_arity then basic_check last_env codom else ()
+
+(* 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 cumi paramsctxt env_ar inds =
+  let numparams = rel_context_nhyps paramsctxt 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.CumulativityInfo.univ_context cumi in
+  let uctx_other = Univ.UContext.make (other_instnace, Univ.UContext.constraints uctx) 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
+      | RegularArity { mind_user_arity = full_arity} ->
+        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
+    
 (************************************************************************)
 (************************************************************************)
 
 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 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 *)
@@ -547,6 +601,14 @@ let check_inductive env kn mib =
   let env_ar = typecheck_arity env params mib.mind_packets in
   (*  - check constructor types *)
   Array.iter (typecheck_one_inductive env_ar params mib) mib.mind_packets;
+  (* check the inferred subtyping relation *)
+  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 f890adba9a..e1860a23f0 100644
--- a/checker/inductive.ml
+++ b/checker/inductive.ml
@@ -54,10 +54,31 @@ let inductive_params (mib,_) = mib.mind_nparams
 
 (** Polymorphic inductives *)
 
-let inductive_instance mib =
-  if mib.mind_polymorphic then
-    UContext.instance mib.mind_universes
-  else Instance.empty
+let inductive_is_polymorphic mib =
+  match mib.mind_universes with
+  | Monomorphic_ind _ -> false
+  | Polymorphic_ind ctx -> true
+  | Cumulative_ind cumi -> true
+
+let inductive_is_cumulative mib =
+  match mib.mind_universes with
+  | Monomorphic_ind _ -> false
+  | Polymorphic_ind ctx -> false
+  | Cumulative_ind cumi -> true
+
+let inductive_polymorphic_instance mib =
+  match mib.mind_universes with
+  | Monomorphic_ind _ -> Univ.Instance.empty
+  | Polymorphic_ind ctx -> Univ.AUContext.instance ctx
+  | Cumulative_ind cumi -> 
+    Univ.AUContext.instance (Univ.ACumulativityInfo.univ_context cumi)
+
+let inductive_polymorphic_context mib =
+  match mib.mind_universes with
+  | Monomorphic_ind _ -> Univ.UContext.empty
+  | Polymorphic_ind ctx -> Univ.instantiate_univ_context ctx
+  | Cumulative_ind cumi -> 
+    Univ.instantiate_univ_context (Univ.ACumulativityInfo.univ_context cumi)
 
 (************************************************************************)
 
@@ -93,7 +114,7 @@ let instantiate_params full t u args sign =
 
 let full_inductive_instantiate mib u params sign =
   let dummy = Prop Null in
-  let t = mkArity (subst_instance_context u sign,dummy) in
+  let t = mkArity (Term.subst_instance_context u sign,dummy) in
     fst (destArity (instantiate_params true t u params mib.mind_params_ctxt))
 
 let full_constructor_instantiate ((mind,_),u,(mib,_),params) t =
@@ -199,7 +220,7 @@ let instantiate_universes env ctx ar argsorts =
 let type_of_inductive_gen env ((mib,mip),u) paramtyps =
   match mip.mind_arity with
   | RegularArity a ->
-    if not mib.mind_polymorphic then a.mind_user_arity
+    if not (inductive_is_polymorphic mib) then a.mind_user_arity
     else subst_instance_constr u a.mind_user_arity
   | TemplateArity ar ->
     let ctx = List.rev mip.mind_arity_ctxt in
diff --git a/checker/inductive.mli b/checker/inductive.mli
index ed3a7b53ce..9a5541f39b 100644
--- a/checker/inductive.mli
+++ b/checker/inductive.mli
@@ -22,7 +22,13 @@ type mind_specif = mutual_inductive_body * one_inductive_body
     Raises [Not_found] if the inductive type is not found. *)
 val lookup_mind_specif : env -> inductive -> mind_specif
 
-val inductive_instance : mutual_inductive_body -> Univ.universe_instance
+val inductive_is_polymorphic : mutual_inductive_body -> bool
+
+val inductive_is_cumulative : mutual_inductive_body -> bool
+
+val inductive_polymorphic_instance : mutual_inductive_body -> Univ.universe_instance
+
+val inductive_polymorphic_context : mutual_inductive_body -> Univ.universe_context
 
 val type_of_inductive : env -> mind_specif puniverses -> constr
 
diff --git a/checker/mod_checking.ml b/checker/mod_checking.ml
index 7f93e15609..15e9ae2951 100644
--- a/checker/mod_checking.ml
+++ b/checker/mod_checking.ml
@@ -1,4 +1,3 @@
-
 open Pp
 open Util
 open Names
@@ -26,21 +25,23 @@ let refresh_arity ar =
     | _ -> ar, Univ.ContextSet.empty
 
 let check_constant_declaration env kn cb =
-  Flags.if_verbose Feedback.msg_notice (str "  checking cst: " ++ prcon kn);
-  let env' =
-    if cb.const_polymorphic then
-      let inst = Univ.make_abstract_instance cb.const_universes in
-      let ctx = Univ.UContext.make (inst, Univ.UContext.constraints cb.const_universes) in
-        push_context ~strict:false ctx env
-    else push_context ~strict:true cb.const_universes env
+  Feedback.msg_notice (str "  checking cst:" ++ prcon kn);
+  let env', u =
+    match cb.const_universes with
+    | Monomorphic_const ctx -> push_context ~strict:true ctx env, Univ.Instance.empty
+    | Polymorphic_const auctx ->
+      let ctx = Univ.instantiate_univ_context auctx in
+      push_context ~strict:false ctx env, Univ.UContext.instance ctx
   in
   let envty, ty = 
     match cb.const_type with
       RegularArity ty ->
+        let ty = subst_instance_constr u ty in
         let ty', cu = refresh_arity ty in
         let envty = push_context_set cu env' in
         let _ = infer_type envty ty' in envty, ty
     | TemplateArity(ctxt,par) ->
+        assert(Univ.Instance.is_empty u);
         let _ = check_ctxt env' ctxt in
         check_polymorphic_arity env' ctxt par;
 	env', it_mkProd_or_LetIn (Sort(Type par.template_level)) ctxt 
@@ -48,6 +49,7 @@ let check_constant_declaration env kn cb =
   let () = 
     match body_of_constant cb with
     | Some bd ->
+      let bd = subst_instance_constr u bd in
       (match cb.const_proj with 
       | None -> let j = infer envty bd in
 		  conv_leq envty j ty
@@ -57,7 +59,7 @@ let check_constant_declaration env kn cb =
 	  conv_leq envty j ty)
     | None -> ()
   in
-  if cb.const_polymorphic then add_constant kn cb env
+  if constant_is_polymorphic cb then add_constant kn cb env
   else add_constant kn cb env'
 
 (** {6 Checking modules } *)
diff --git a/checker/modops.ml b/checker/modops.ml
index bed31143bf..be35c7e981 100644
--- a/checker/modops.ml
+++ b/checker/modops.ml
@@ -83,10 +83,10 @@ let strengthen_const mp_from l cb resolver =
     | Def _ -> cb
     | _ ->
       let con = Constant.make2 mp_from l in
-      let u = 
-	if cb.const_polymorphic then
-	  Univ.make_abstract_instance cb.const_universes
-	else Univ.Instance.empty
+      let u =
+        match cb.const_universes with
+      | Monomorphic_const _ -> Univ.Instance.empty
+      | Polymorphic_const auctx -> Univ.make_abstract_instance auctx
       in
       { cb with
 	const_body = Def (Declarations.from_val (Const (con,u))) }
diff --git a/checker/reduction.ml b/checker/reduction.ml
index ba0b017844..95dc93f5d2 100644
--- a/checker/reduction.ml
+++ b/checker/reduction.ml
@@ -117,6 +117,10 @@ let beta_appvect c v =
 (*                         Conversion                               *)
 (********************************************************************)
 
+type conv_pb =
+  | CONV
+  | CUMUL
+
 (* Conversion utility functions *)
 type 'a conversion_function = env -> 'a -> 'a -> unit
 
@@ -152,11 +156,62 @@ let compare_stacks f fmind lft1 stk1 lft2 stk2 =
     cmp_rec (pure_stack lft1 stk1) (pure_stack lft2 stk2)
   else raise NotConvertible
 
-(* Convertibility of sorts *)
+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!")
+  else
+    let comp_cst =
+      let comp_subst = (Univ.Instance.append u u') in
+      Univ.UContext.constraints
+      (Univ.subst_instance_context comp_subst ind_subtypctx)
+    in
+    let comp_cst =
+      match cv_pb with
+        CONV ->
+        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
+    if (Univ.check_constraints comp_cst univs) then () else raise NotConvertible
+
+let convert_inductives
+    cv_pb (mind, ind) u1 sv1 u2 sv2 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 =
+  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
+    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
 
-type conv_pb =
-  | CONV
-  | CUMUL
+(* Convertibility of sorts *)
 
 let sort_cmp env univ pb s0 s1 =
   match (s0,s1) with
@@ -375,18 +430,37 @@ and eqappr univ cv_pb infos (lft1,st1) (lft2,st2) =
     (* Inductive types:  MutInd MutConstruct Fix Cofix *)
 
     | (FInd (ind1,u1), FInd (ind2,u2)) ->
-        if mind_equiv_infos infos ind1 ind2
-	then
-	  (let () = convert_universes univ u1 u2 in
-           convert_stacks univ infos lft1 lft2 v1 v2)
-        else raise NotConvertible
-
-     | (FConstruct ((ind1,j1),u1), FConstruct ((ind2,j2),u2)) ->
-	 if Int.equal j1 j2 && mind_equiv_infos infos ind1 ind2
-	 then
-	  (let () = convert_universes univ u1 u2 in
-           convert_stacks univ infos lft1 lft2 v1 v2)
-         else raise NotConvertible
+      if mind_equiv_infos infos ind1 ind2 then
+        if Univ.Instance.length u1 = 0 || Univ.Instance.length u2 = 0 then
+          begin
+            convert_universes univ u1 u2;
+            convert_stacks univ infos lft1 lft2 v1 v2
+          end
+        else
+          let mind = Environ.lookup_mind (fst ind1) (infos_env infos) in
+          let () =
+            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
+
+    | (FConstruct ((ind1,j1),u1), FConstruct ((ind2,j2),u2)) ->
+      if Int.equal j1 j2 && mind_equiv_infos infos ind1 ind2 then
+        if Univ.Instance.length u1 = 0 || Univ.Instance.length u2 = 0 then
+          begin
+            convert_universes univ u1 u2;
+            convert_stacks univ infos lft1 lft2 v1 v2
+          end
+        else
+          let mind = Environ.lookup_mind (fst ind1) (infos_env infos) in
+          let () =
+            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
 
      (* Eta expansion of records *)
      | (FConstruct ((ind1,j1),u1), _) ->
diff --git a/checker/subtyping.ml b/checker/subtyping.ml
index 2d04b77e46..bfe19584a7 100644
--- a/checker/subtyping.ml
+++ b/checker/subtyping.ml
@@ -88,18 +88,25 @@ let check_inductive  env mp1 l info1 mib2 spec2 subst1 subst2=
   let check_conv f = check_conv_error error f in
   let mib1 =
     match info1 with
-      | IndType ((_,0), mib) -> mib
+      | IndType ((_,0), mib) -> subst_mind subst1 mib
       | _ -> error ()
   in
   let mib2 = subst_mind subst2 mib2 in
   let check eq f = if not (eq (f mib1) (f mib2)) then error () in
-  let bool_equal (x : bool) (y : bool) = x = y in
-  let u = 
-    check bool_equal (fun x -> x.mind_polymorphic);
-    if mib1.mind_polymorphic then (
-      check Univ.Instance.equal (fun x -> Univ.UContext.instance x.mind_universes);
-      Univ.UContext.instance 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/term.ml b/checker/term.ml
index 75c566aeb7..dea3d3e659 100644
--- a/checker/term.ml
+++ b/checker/term.ml
@@ -227,6 +227,8 @@ let rel_context_nhyps hyps =
   nhyps 0 hyps
 let fold_rel_context f l ~init = List.fold_right f l init
 
+let fold_rel_context_outside f l ~init = List.fold_right f l init
+
 let map_rel_decl f = function
   | LocalAssum (n, typ) as decl ->
      let typ' = f typ in
@@ -414,6 +416,42 @@ let subst_instance_constr subst c =
   if Univ.Instance.is_empty subst then c
   else
     let f u = Univ.subst_instance_instance subst u in
+    let rec aux t =
+      match t with
+      | Const (c, u) ->
+       if Univ.Instance.is_empty u then t
+       else
+          let u' = f u in
+           if u' == u then t
+           else (Const (c, u'))
+      | Ind (i, u) ->
+       if Univ.Instance.is_empty u then t
+       else
+         let u' = f u in
+           if u' == u then t
+           else (Ind (i, u'))
+      | Construct (c, u) ->
+       if Univ.Instance.is_empty u then t
+       else
+          let u' = f u in
+           if u' == u then t
+           else (Construct (c, u'))
+      | Sort (Type u) ->
+         let u' = Univ.subst_instance_universe subst u in
+          if u' == u then t else
+            (Sort (sort_of_univ u'))
+      | _ -> map_constr aux t
+    in
+    aux c
+
+let subst_instance_context s ctx = 
+  if Univ.Instance.is_empty s then ctx
+  else map_rel_context (fun x -> subst_instance_constr s x) ctx
+
+let subst_univs_level_constr subst c =
+  if Univ.is_empty_level_subst subst then c
+  else 
+    let f = Univ.Instance.subst_fn (Univ.subst_univs_level_level subst) in
     let changed = ref false in
     let rec aux t = 
       match t with
@@ -436,14 +474,10 @@ let subst_instance_constr subst c =
 	    if u' == u then t
 	    else (changed := true; Construct (c, u'))
       | Sort (Type u) -> 
-         let u' = Univ.subst_instance_universe subst u in
+         let u' = Univ.subst_univs_level_universe subst u in
 	   if u' == u then t else 
 	     (changed := true; Sort (sort_of_univ u'))
       | _ -> map_constr aux t
     in
     let c' = aux c in
       if !changed then c' else c
-
-let subst_instance_context s ctx = 
-  if Univ.Instance.is_empty s then ctx
-  else map_rel_context (fun x -> subst_instance_constr s x) ctx
diff --git a/checker/term.mli b/checker/term.mli
index 6b026d056f..ccf5b59e0c 100644
--- a/checker/term.mli
+++ b/checker/term.mli
@@ -33,6 +33,8 @@ val rel_context_length : rel_context -> int
 val rel_context_nhyps : rel_context -> int
 val fold_rel_context :
   (rel_declaration -> 'a -> 'a) -> rel_context -> init:'a -> 'a
+val fold_rel_context_outside :
+  (rel_declaration -> 'a -> 'a) -> rel_context -> init:'a -> 'a
 val map_rel_decl : (constr -> constr) -> rel_declaration -> rel_declaration
 val map_rel_context : (constr -> constr) -> rel_context -> rel_context
 val extended_rel_list : int -> rel_context -> constr list
@@ -55,3 +57,4 @@ val eq_constr : constr -> constr -> bool
 (** Instance substitution for polymorphism. *)
 val subst_instance_constr : Univ.universe_instance -> constr -> constr
 val subst_instance_context : Univ.universe_instance -> rel_context -> rel_context
+val subst_univs_level_constr : Univ.universe_level_subst -> constr -> constr
diff --git a/checker/typeops.ml b/checker/typeops.ml
index 0163db3347..543f9acced 100644
--- a/checker/typeops.ml
+++ b/checker/typeops.ml
@@ -329,7 +329,6 @@ let rec execute env cstr =
         let pj = execute env p in
         let lfj = execute_array env lf in
         judge_of_case env ci (p,pj) (c,cj) lfj
-
     | Fix ((_,i as vni),recdef) ->
         let fix_ty = execute_recdef env recdef i in
         let fix = (vni,recdef) in
diff --git a/checker/univ.ml b/checker/univ.ml
index 5717432315..0ee4686c1a 100644
--- a/checker/univ.ml
+++ b/checker/univ.ml
@@ -968,7 +968,23 @@ struct
       else Level.compare v v'
 end
 
-module Constraint = Set.Make(UConstraintOrd)
+let pr_constraint_type op = 
+  let op_str = match op with
+    | Lt -> " < "
+    | Le -> " <= "
+    | Eq -> " = "
+  in str op_str
+
+module Constraint = 
+struct 
+  module S = Set.Make(UConstraintOrd)
+  include S
+
+  let pr prl c =
+    fold (fun (u1,op,u2) pp_std ->
+      pp_std ++ prl u1 ++ pr_constraint_type op ++
+	prl u2 ++ fnl () )  c (str "")
+end
 
 let empty_constraint = Constraint.empty
 let merge_constraints c g =
@@ -1056,7 +1072,9 @@ module Instance : sig
     val subst_fn : universe_level_subst_fn -> t -> t
     val subst : universe_level_subst -> t -> t
     val pr : t -> Pp.std_ppcmds
-    val check_eq : t check_function 
+    val check_eq : t check_function
+    val length : t -> int
+    val append : t -> t -> t
 end = 
 struct
   type t = Level.t array
@@ -1099,6 +1117,7 @@ struct
 	(* [h] must be positive. *)
 	let h = !accu land 0x3FFFFFFF in
 	  h
+
   end
 
   module HInstance = Hashcons.Make(HInstancestruct)
@@ -1135,6 +1154,10 @@ struct
 	   (Int.equal i (Array.length t1)) || (check_eq_level g t1.(i) t2.(i) && aux (i + 1))
 	 in aux 0)
 
+  let length = Array.length
+
+  let append = Array.append
+  
 end
 
 type universe_instance = Instance.t
@@ -1152,10 +1175,63 @@ struct
   let make x = x
   let instance (univs, cst) = univs
   let constraints (univs, cst) = cst
+
+  let is_empty (univs, cst) = Instance.is_empty univs && Constraint.is_empty cst
+  let pr prl (univs, cst as ctx) =
+    if is_empty ctx then mt() else
+      h 0 (Instance.pr univs ++ str " |= ") ++ h 0 (v 0 (Constraint.pr prl cst))
 end
 
 type universe_context = UContext.t
 
+module AUContext = UContext
+
+type abstract_universe_context = AUContext.t
+
+module CumulativityInfo =
+struct
+  type t = universe_context * universe_context
+
+  let make x =
+    if (Array.length (UContext.instance (snd x))) =
+       (Array.length (UContext.instance (fst x))) * 2 then x
+    else anomaly (Pp.str "Invalid subtyping information encountered!")
+
+  let empty = (UContext.empty, UContext.empty)
+
+  let halve_context ctx =
+    let len = Array.length ctx in
+    let halflen = len / 2 in
+    ((Array.sub ctx 0 halflen), (Array.sub ctx halflen halflen))
+
+  let univ_context (univcst, subtypcst) = univcst
+  let subtyp_context (univcst, subtypcst) = subtypcst
+
+  let create_trivial_subtyping ctx ctx' =
+    CArray.fold_left_i
+      (fun i cst l -> Constraint.add (l, Eq, Array.get ctx' i) cst)
+      Constraint.empty ctx
+
+  let from_universe_context univcst freshunivs =
+    let inst = (UContext.instance univcst) in
+    assert (Array.length freshunivs = Array.length inst);
+    (univcst, UContext.make (Array.append inst freshunivs,
+                             create_trivial_subtyping inst freshunivs))
+
+  let subtyping_other_instance (univcst, subtypcst) =
+    let (_, ctx') = (halve_context (UContext.instance subtypcst)) in ctx'
+  
+  let subtyping_susbst (univcst, subtypcst) =
+    let (ctx, ctx') = (halve_context (UContext.instance subtypcst)) in
+    Array.fold_left2 (fun subst l1 l2 -> LMap.add l1 l2 subst) LMap.empty ctx ctx'
+
+end
+
+type cumulativity_info = CumulativityInfo.t
+
+module ACumulativityInfo = CumulativityInfo
+type abstract_cumulativity_info = ACumulativityInfo.t
+
 module ContextSet =
 struct
   type t = LSet.t constrained
@@ -1166,6 +1242,8 @@ struct
 end
 type universe_context_set = ContextSet.t
 
+
+
 (** Substitutions. *)
 
 let is_empty_subst = LMap.is_empty
@@ -1210,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
@@ -1219,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
@@ -1262,6 +1343,10 @@ let merge_context_set strict ctx g =
 
 (** Pretty-printing *)
 
+let pr_constraints prl = Constraint.pr prl
+    
+let pr_universe_context = UContext.pr
+
 let pr_arc = function
   | _, Canonical {univ=u; lt=[]; le=[]} ->
       mt ()
diff --git a/checker/univ.mli b/checker/univ.mli
index 7d4c629ab9..a503924708 100644
--- a/checker/univ.mli
+++ b/checker/univ.mli
@@ -18,6 +18,9 @@ sig
   (** Create a new universe level from a unique identifier and an associated
       module path. *)
 
+  val pr : t -> Pp.std_ppcmds
+  (** Pretty-printing *)
+  
   val equal : t -> t -> bool
 end
 
@@ -71,6 +74,8 @@ type 'a check_function = universes -> 'a -> 'a -> bool
 val check_leq : universe check_function
 val check_eq : universe check_function
 
+
+
 (** The initial graph of universes: Prop < Set *)
 val initial_universes : universes
 
@@ -170,6 +175,12 @@ sig
 
   val check_eq : t check_function
   (** Check equality of instances w.r.t. a universe graph *)
+
+  val length : t -> int
+  (** Compute the length of the instance  *)
+
+  val append : t -> t -> t
+  (** Append two universe instances *)
 end
 
 type universe_instance = Instance.t
@@ -187,9 +198,54 @@ sig
   val make : universe_instance constrained -> t
   val instance : t -> Instance.t
   val constraints : t -> constraints
+  val is_empty : t -> bool
+    
+end
+
+type universe_context = UContext.t
+
+module AUContext :
+sig
+  type t
+
+  val instance : t -> Instance.t
+
+end
+
+type abstract_universe_context = AUContext.t
+
+module CumulativityInfo :
+sig
+  type t
+
+  val make : universe_context * universe_context -> t
+
+  val empty : t
+
+  val univ_context : t -> universe_context
+  val subtyp_context : t -> universe_context
+
+  val from_universe_context : universe_context -> universe_instance -> t
+
+  val subtyping_other_instance : t -> universe_instance
+  
+  val subtyping_susbst : t -> universe_level_subst
+
+end
+
+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 
     type t
@@ -198,7 +254,6 @@ module ContextSet :
     val constraints : t -> constraints
   end
 
-type universe_context = UContext.t
 type universe_context_set = ContextSet.t
 
 val merge_context : bool -> universe_context -> universes -> universes
@@ -221,18 +276,22 @@ 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. } *)
 
+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_universes : universes -> Pp.std_ppcmds
diff --git a/checker/values.ml b/checker/values.ml
index c175aed680..b8b395aaf7 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 6466d8cc443b5896cb905776df0cc49e  checker/cic.mli
+MD5 b132075590daf5e202de0d9cc34e6003  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,8 +278,7 @@ let v_ind_pack = v_tuple "mutual_inductive_body"
     Int;
     Int;
     v_rctxt;
-    v_bool;
-    v_context;
+    v_ind_pack_univs; (* universes *)
     Opt v_bool;
     v_typing_flags|]