From a9f0fd89cf3bb4b728eb451572a96f8599211380 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Wed, 30 Jan 2019 14:39:28 +0100
Subject: Separate variance and universe fields in inductives.

I think the usage looks cleaner this way.
---
 kernel/cbytegen.ml     |  6 +----
 kernel/cbytegen.mli    |  2 +-
 kernel/cooking.ml      | 12 ++++-----
 kernel/cooking.mli     |  2 +-
 kernel/declarations.ml | 17 +++++-------
 kernel/declareops.ml   | 56 +++++++++++++++++++---------------------
 kernel/declareops.mli  |  4 +++
 kernel/entries.ml      | 24 ++++++++---------
 kernel/indTyping.ml    | 50 ++++++++++++++++--------------------
 kernel/indTyping.mli   |  3 ++-
 kernel/indtypes.ml     | 13 ++++------
 kernel/inductive.ml    |  7 +----
 kernel/mod_typing.ml   |  8 +++---
 kernel/modops.ml       |  7 ++---
 kernel/modops.mli      |  1 +
 kernel/nativecode.ml   |  6 +----
 kernel/reduction.ml    | 22 +++++-----------
 kernel/safe_typing.ml  | 29 ++++++++++-----------
 kernel/subtyping.ml    | 63 +++++++++++++++++----------------------------
 kernel/term_typing.ml  | 34 ++++++++++--------------
 kernel/univ.ml         | 70 --------------------------------------------------
 kernel/univ.mli        | 44 -------------------------------
 22 files changed, 153 insertions(+), 327 deletions(-)

(limited to 'kernel')

diff --git a/kernel/cbytegen.ml b/kernel/cbytegen.ml
index b95a940c14..718584b3d4 100644
--- a/kernel/cbytegen.ml
+++ b/kernel/cbytegen.ml
@@ -881,11 +881,7 @@ let compile_constant_body ~fail_on_error env univs = function
   | Undef _ | OpaqueDef _ | Primitive _ -> Some BCconstant
   | Def sb ->
       let body = Mod_subst.force_constr sb in
-      let instance_size =
-        match univs with
-        | Monomorphic_const _ -> 0
-        | Polymorphic_const univ -> Univ.AUContext.size univ
-      in
+      let instance_size = Univ.AUContext.size (Declareops.universes_context univs) in
       match kind body with
 	| Const (kn',u) when is_univ_copy instance_size u ->
 	    (* we use the canonical name of the constant*)
diff --git a/kernel/cbytegen.mli b/kernel/cbytegen.mli
index b1b55aef48..6a9550342c 100644
--- a/kernel/cbytegen.mli
+++ b/kernel/cbytegen.mli
@@ -20,7 +20,7 @@ val compile : fail_on_error:bool ->
 (** init, fun, fv *)
 
 val compile_constant_body : fail_on_error:bool ->
-  env -> constant_universes -> Constr.t Mod_subst.substituted constant_def ->
+  env -> universes -> Constr.t Mod_subst.substituted 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 88586352f6..22de9bfad5 100644
--- a/kernel/cooking.ml
+++ b/kernel/cooking.ml
@@ -157,7 +157,7 @@ type inline = bool
 type result = {
   cook_body : constr Mod_subst.substituted constant_def;
   cook_type : types;
-  cook_universes : constant_universes;
+  cook_universes : universes;
   cook_private_univs : Univ.ContextSet.t option;
   cook_inline : inline;
   cook_context : Constr.named_context option;
@@ -185,10 +185,10 @@ let cook_constr { Opaqueproof.modlist ; abstract = (vars, subst, _) } c =
 
 let lift_univs cb subst auctx0 =
   match cb.const_universes with
-  | Monomorphic_const ctx ->
+  | Monomorphic ctx ->
     assert (AUContext.is_empty auctx0);
-    subst, (Monomorphic_const ctx)
-  | Polymorphic_const auctx ->
+    subst, (Monomorphic ctx)
+  | Polymorphic auctx ->
     (** Given a named instance [subst := u₀ ... uₙ₋₁] together with an abstract
         context [auctx0 := 0 ... n - 1 |= C{0, ..., n - 1}] of the same length,
         and another abstract context relative to the former context
@@ -202,13 +202,13 @@ let lift_univs cb subst auctx0 =
     *)
     if (Univ.Instance.is_empty subst) then
       (** Still need to take the union for the constraints between globals *)
-      subst, (Polymorphic_const (AUContext.union auctx0 auctx))
+      subst, (Polymorphic (AUContext.union auctx0 auctx))
     else
       let ainst = Univ.make_abstract_instance auctx in
       let subst = Instance.append subst ainst in
       let substf = Univ.make_instance_subst subst in
       let auctx' = Univ.subst_univs_level_abstract_universe_context substf auctx in
-      subst, (Polymorphic_const (AUContext.union auctx0 auctx'))
+      subst, (Polymorphic (AUContext.union auctx0 auctx'))
 
 let cook_constant ~hcons { from = cb; info } =
   let { Opaqueproof.modlist; abstract } = info in
diff --git a/kernel/cooking.mli b/kernel/cooking.mli
index 07c6f37fab..89b5c60ad5 100644
--- a/kernel/cooking.mli
+++ b/kernel/cooking.mli
@@ -20,7 +20,7 @@ type inline = bool
 type result = {
   cook_body : constr Mod_subst.substituted constant_def;
   cook_type : types;
-  cook_universes : constant_universes;
+  cook_universes : universes;
   cook_private_univs : Univ.ContextSet.t option;
   cook_inline : inline;
   cook_context : Constr.named_context option;
diff --git a/kernel/declarations.ml b/kernel/declarations.ml
index 1008492825..6777e0c223 100644
--- a/kernel/declarations.ml
+++ b/kernel/declarations.ml
@@ -53,9 +53,9 @@ type 'a constant_def =
   | OpaqueDef of Opaqueproof.opaque       (** or an opaque global definition *)
   | Primitive of CPrimitives.t            (** or a primitive operation *)
 
-type constant_universes =
-  | Monomorphic_const of Univ.ContextSet.t
-  | Polymorphic_const of Univ.AUContext.t
+type universes =
+  | Monomorphic of Univ.ContextSet.t
+  | Polymorphic of Univ.AUContext.t
 
 (** The [typing_flags] are instructions to the type-checker which
     modify its behaviour. The typing flags used in the type-checking
@@ -92,7 +92,7 @@ type constant_body = {
     const_body : Constr.t Mod_subst.substituted constant_def;
     const_type : types;
     const_body_code : Cemitcodes.to_patch_substituted option;
-    const_universes : constant_universes;
+    const_universes : universes;
     const_private_poly_univs : Univ.ContextSet.t option;
     const_inline_code : bool;
     const_typing_flags : typing_flags; (** The typing options which
@@ -185,11 +185,6 @@ type one_inductive_body = {
     mind_reloc_tbl :  Vmvalues.reloc_table;
   }
 
-type abstract_inductive_universes =
-  | Monomorphic_ind of Univ.ContextSet.t
-  | Polymorphic_ind of Univ.AUContext.t
-  | Cumulative_ind of Univ.ACumulativityInfo.t
-
 type recursivity_kind =
   | Finite (** = inductive *)
   | CoFinite (** = coinductive *)
@@ -213,7 +208,9 @@ type mutual_inductive_body = {
 
     mind_params_ctxt : Constr.rel_context;  (** The context of parameters (includes let-in declaration) *)
 
-    mind_universes : abstract_inductive_universes; (** Information about monomorphic/polymorphic/cumulative inductives and their universes *)
+    mind_universes : universes; (** Information about monomorphic/polymorphic/cumulative inductives and their universes *)
+
+    mind_variance : Univ.Variance.t array option; (** Variance info, [None] when non-cumulative. *)
 
     mind_private : bool option; (** allow pattern-matching: Some true ok, Some false blocked *)
 
diff --git a/kernel/declareops.ml b/kernel/declareops.ml
index 5686c4071d..9e0230c3ba 100644
--- a/kernel/declareops.ml
+++ b/kernel/declareops.ml
@@ -49,12 +49,24 @@ let hcons_template_arity ar =
       (* List.Smart.map (Option.Smart.map Univ.hcons_univ_level) ar.template_param_levels; *)
     template_level = Univ.hcons_univ ar.template_level }
 
+let universes_context = function
+  | Monomorphic _ -> Univ.AUContext.empty
+  | Polymorphic ctx -> ctx
+
+let abstract_universes = function
+  | Entries.Monomorphic_entry ctx ->
+    Univ.empty_level_subst, Monomorphic ctx
+  | Entries.Polymorphic_entry (nas, ctx) ->
+    let (inst, auctx) = Univ.abstract_universes nas ctx in
+    let inst = Univ.make_instance_subst inst in
+    (inst, Polymorphic auctx)
+
 (** {6 Constants } *)
 
 let constant_is_polymorphic cb =
   match cb.const_universes with
-  | Monomorphic_const _ -> false
-  | Polymorphic_const _ -> true
+  | Monomorphic _ -> false
+  | Polymorphic _ -> true
 
 
 let constant_has_body cb = match cb.const_body with
@@ -62,9 +74,7 @@ let constant_has_body cb = match cb.const_body with
   | Def _ | OpaqueDef _ -> true
 
 let constant_polymorphic_context cb =
-  match cb.const_universes with
-  | Monomorphic_const _ -> Univ.AUContext.empty
-  | Polymorphic_const ctx -> ctx
+  universes_context cb.const_universes
 
 let is_opaque cb = match cb.const_body with
   | OpaqueDef _ -> true
@@ -126,12 +136,12 @@ let hcons_const_def = function
     Def (from_val (Constr.hcons constr))
   | OpaqueDef _ as x -> x (* hashconsed when turned indirect *)
 
-let hcons_const_universes cbu =
+let hcons_universes cbu =
   match cbu with
-  | Monomorphic_const ctx -> 
-    Monomorphic_const (Univ.hcons_universe_context_set ctx)
-  | Polymorphic_const ctx ->
-    Polymorphic_const (Univ.hcons_abstract_universe_context ctx)
+  | Monomorphic ctx ->
+    Monomorphic (Univ.hcons_universe_context_set ctx)
+  | Polymorphic ctx ->
+    Polymorphic (Univ.hcons_abstract_universe_context ctx)
 
 let hcons_const_private_univs = function
   | None -> None
@@ -141,7 +151,7 @@ let hcons_const_body cb =
   { cb with
     const_body = hcons_const_def cb.const_body;
     const_type = Constr.hcons cb.const_type;
-    const_universes = hcons_const_universes cb.const_universes;
+    const_universes = hcons_universes cb.const_universes;
     const_private_poly_univs = hcons_const_private_univs cb.const_private_poly_univs;
   }
 
@@ -239,27 +249,21 @@ let subst_mind_body sub mib =
       Context.Rel.map (subst_mps sub) mib.mind_params_ctxt;
     mind_packets = Array.Smart.map (subst_mind_packet sub) mib.mind_packets ;
     mind_universes = mib.mind_universes;
+    mind_variance = mib.mind_variance;
     mind_private = mib.mind_private;
     mind_typing_flags = mib.mind_typing_flags;
   }
 
 let inductive_polymorphic_context mib =
-  match mib.mind_universes with
-  | Monomorphic_ind _ -> Univ.AUContext.empty
-  | Polymorphic_ind ctx -> ctx
-  | Cumulative_ind cumi -> Univ.ACumulativityInfo.univ_context cumi
+  universes_context mib.mind_universes
 
 let inductive_is_polymorphic mib =
   match mib.mind_universes with
-  | Monomorphic_ind _ -> false
-  | Polymorphic_ind _ctx -> true
-  | Cumulative_ind _cumi -> true
+  | Monomorphic _ -> false
+  | Polymorphic _ctx -> true
 
 let inductive_is_cumulative mib =
-  match mib.mind_universes with
-  | Monomorphic_ind _ -> false
-  | Polymorphic_ind _ctx -> false
-  | Cumulative_ind _cumi -> true
+  Option.has_some mib.mind_variance
 
 let inductive_make_projection ind mib ~proj_arg =
   match mib.mind_record with
@@ -306,17 +310,11 @@ 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_set 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.Smart.map hcons_mind_packet mib.mind_packets;
     mind_params_ctxt = hcons_rel_context mib.mind_params_ctxt;
-    mind_universes = hcons_mind_universes mib.mind_universes }
+    mind_universes = hcons_universes mib.mind_universes }
 
 (** Hashconsing of modules *)
 
diff --git a/kernel/declareops.mli b/kernel/declareops.mli
index 35490ceef9..23a44433b3 100644
--- a/kernel/declareops.mli
+++ b/kernel/declareops.mli
@@ -15,6 +15,10 @@ open Univ
 (** Operations concerning types in [Declarations] :
     [constant_body], [mutual_inductive_body], [module_body] ... *)
 
+val universes_context : universes -> AUContext.t
+
+val abstract_universes : Entries.universes_entry -> Univ.universe_level_subst * universes
+
 (** {6 Arities} *)
 
 val map_decl_arity : ('a -> 'c) -> ('b -> 'd) ->
diff --git a/kernel/entries.ml b/kernel/entries.ml
index 013327599d..a3d32267a7 100644
--- a/kernel/entries.ml
+++ b/kernel/entries.ml
@@ -16,6 +16,12 @@ open Constr
    constants/axioms, mutual inductive definitions, modules and module
    types *)
 
+type universes_entry =
+  | Monomorphic_entry of Univ.ContextSet.t
+  | Polymorphic_entry of Name.t array * Univ.UContext.t
+
+type 'a in_universes_entry = 'a * universes_entry
+
 (** {6 Declaration of inductive types. } *)
 
 (** Assume the following definition in concrete syntax:
@@ -28,11 +34,6 @@ 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.ContextSet.t
-  | Polymorphic_ind_entry of Name.t array * Univ.UContext.t
-  | Cumulative_ind_entry of Name.t array * Univ.CumulativityInfo.t
-
 type one_inductive_entry = {
   mind_entry_typename : Id.t;
   mind_entry_arity : constr;
@@ -48,7 +49,8 @@ type mutual_inductive_entry = {
   mind_entry_finite : Declarations.recursivity_kind;
   mind_entry_params : Constr.rel_context;
   mind_entry_inds : one_inductive_entry list;
-  mind_entry_universes : inductive_universes;
+  mind_entry_universes : universes_entry;
+  mind_entry_variance : Univ.Variance.t array option;
   (* universe constraints and the constraints for subtyping of
      inductive types in the block. *)
   mind_entry_private : bool option;
@@ -58,12 +60,6 @@ type mutual_inductive_entry = {
 type 'a proof_output = constr Univ.in_universe_context_set * 'a
 type 'a const_entry_body = 'a proof_output Future.computation
 
-type constant_universes_entry =
-  | Monomorphic_const_entry of Univ.ContextSet.t
-  | Polymorphic_const_entry of Name.t array * Univ.UContext.t
-
-type 'a in_constant_universes_entry = 'a * constant_universes_entry
-
 type 'a definition_entry = {
   const_entry_body   : 'a const_entry_body;
   (* List of section variables *)
@@ -71,7 +67,7 @@ type 'a definition_entry = {
   (* State id on which the completion of type checking is reported *)
   const_entry_feedback : Stateid.t option;
   const_entry_type        : types option;
-  const_entry_universes   : constant_universes_entry;
+  const_entry_universes   : universes_entry;
   const_entry_opaque      : bool;
   const_entry_inline_code : bool }
 
@@ -85,7 +81,7 @@ type section_def_entry = {
 type inline = int option (* inlining level, None for no inlining *)
 
 type parameter_entry = 
-    Constr.named_context option * types in_constant_universes_entry * inline
+    Constr.named_context option * types in_universes_entry * inline
 
 type primitive_entry = {
   prim_entry_type : types option;
diff --git a/kernel/indTyping.ml b/kernel/indTyping.ml
index 6976b2019d..a5dafc5ab5 100644
--- a/kernel/indTyping.ml
+++ b/kernel/indTyping.ml
@@ -87,23 +87,28 @@ let check_subtyping_arity_constructor env subst arcn numparams is_arity =
   let last_env = Context.Rel.fold_outside check_typ typs ~init:env in
   if not is_arity then basic_check last_env codom else ()
 
-let check_cumulativity univs env_ar params data =
+let check_cumulativity univs variances env_ar params data =
+  let uctx = match univs with
+    | Monomorphic_entry _ -> raise (InductiveError BadUnivs)
+    | Polymorphic_entry (_,uctx) -> uctx
+  in
+  let instance = UContext.instance uctx in
+  if Instance.length instance != Array.length variances then raise (InductiveError BadUnivs);
   let numparams = Context.Rel.nhyps params in
-  let uctx = CumulativityInfo.univ_context univs in
-  let new_levels = Array.init (UContext.size uctx)
+  let new_levels = Array.init (Instance.length instance)
       (fun i -> Level.(make (UGlobal.make DirPath.empty i)))
   in
   let lmap = Array.fold_left2 (fun lmap u u' -> LMap.add u u' lmap)
-      LMap.empty (Instance.to_array @@ UContext.instance uctx) new_levels
+      LMap.empty (Instance.to_array instance) new_levels
   in
   let dosubst = Vars.subst_univs_level_constr lmap in
   let instance_other = Instance.of_array new_levels in
-  let constraints_other = Univ.subst_univs_level_constraints lmap (Univ.UContext.constraints uctx) in
+  let constraints_other = Univ.subst_univs_level_constraints lmap (UContext.constraints uctx) in
   let uctx_other = Univ.UContext.make (instance_other, constraints_other) in
   let env = Environ.push_context uctx_other env_ar in
   let subtyp_constraints =
-    CumulativityInfo.leq_constraints univs
-      (UContext.instance uctx) instance_other
+    Univ.enforce_leq_variance_instances variances
+      instance instance_other
       Constraint.empty
   in
   let env = Environ.add_constraints subtyp_constraints env in
@@ -236,8 +241,8 @@ let abstract_packets univs usubst params ((arity,lc),(indices,splayed_lc),univ_i
     | None -> RegularArity {mind_user_arity=arity;mind_sort=Sorts.sort_of_univ ind_univ}
     | Some min_univ ->
       ((match univs with
-          | Monomorphic_ind _ -> ()
-          | Polymorphic_ind _ | Cumulative_ind _ ->
+          | Monomorphic _ -> ()
+          | Polymorphic _ ->
             CErrors.anomaly ~label:"polymorphic_template_ind"
               Pp.(strbrk "Template polymorphism and full polymorphism are incompatible."));
        TemplateArity {template_param_levels=param_ccls params; template_level=min_univ})
@@ -246,17 +251,6 @@ let abstract_packets univs usubst params ((arity,lc),(indices,splayed_lc),univ_i
   let kelim = allowed_sorts univ_info in
   (arity,lc), (indices,splayed_lc), kelim
 
-let abstract_inductive_universes = function
-  | Monomorphic_ind_entry ctx -> (Univ.empty_level_subst, Monomorphic_ind ctx)
-  | Polymorphic_ind_entry (nas, ctx) ->
-    let (inst, auctx) = Univ.abstract_universes nas ctx in
-    let inst = Univ.make_instance_subst inst in
-    (inst, Polymorphic_ind auctx)
-  | Cumulative_ind_entry (nas, cumi) ->
-    let (inst, acumi) = Univ.abstract_cumulativity_info nas cumi in
-    let inst = Univ.make_instance_subst inst in
-    (inst, Cumulative_ind acumi)
-
 let typecheck_inductive env (mie:mutual_inductive_entry) =
   let () = match mie.mind_entry_inds with
   | [] -> CErrors.anomaly Pp.(str "empty inductive types declaration.")
@@ -269,9 +263,8 @@ let typecheck_inductive env (mie:mutual_inductive_entry) =
   (* universes *)
   let env_univs =
     match mie.mind_entry_universes with
-    | Monomorphic_ind_entry ctx -> push_context_set ctx env
-    | Polymorphic_ind_entry (_, ctx) -> push_context ctx env
-    | Cumulative_ind_entry (_, cumi) -> push_context (Univ.CumulativityInfo.univ_context cumi) env
+    | Monomorphic_entry ctx -> push_context_set ctx env
+    | Polymorphic_entry (_, ctx) -> push_context ctx env
   in
 
   (* Params *)
@@ -287,13 +280,14 @@ let typecheck_inductive env (mie:mutual_inductive_entry) =
       mie.mind_entry_inds data
   in
 
-  let () = match mie.mind_entry_universes with
-    | Cumulative_ind_entry (_,univs) -> check_cumulativity univs env_ar params (List.map pi1 data)
-    | Monomorphic_ind_entry _ | Polymorphic_ind_entry _ -> ()
+  let () = match mie.mind_entry_variance with
+    | None -> ()
+    | Some variances ->
+      check_cumulativity mie.mind_entry_universes variances env_ar params (List.map pi1 data)
   in
 
   (* Abstract universes *)
-  let usubst, univs = abstract_inductive_universes mie.mind_entry_universes in
+  let usubst, univs = Declareops.abstract_universes mie.mind_entry_universes in
   let params = Vars.subst_univs_level_context usubst params in
   let data = List.map (abstract_packets univs usubst params) data in
 
@@ -304,4 +298,4 @@ let typecheck_inductive env (mie:mutual_inductive_entry) =
     Environ.push_rel_context ctx env
   in
 
-  env_ar_par, univs, params, Array.of_list data
+  env_ar_par, univs, mie.mind_entry_variance, params, Array.of_list data
diff --git a/kernel/indTyping.mli b/kernel/indTyping.mli
index 8841e38636..2598548f3f 100644
--- a/kernel/indTyping.mli
+++ b/kernel/indTyping.mli
@@ -16,6 +16,7 @@ open Declarations
     Returns:
     - environment with inductives + parameters in rel context
     - abstracted universes
+    - checked variance info
     - parameters
     - for each inductive,
       (arity * constructors) (with params)
@@ -24,7 +25,7 @@ open Declarations
  *)
 val typecheck_inductive : env -> mutual_inductive_entry ->
   env
-  * abstract_inductive_universes
+  * universes * Univ.Variance.t array option
   * Constr.rel_context
   * ((inductive_arity * Constr.types array) *
      (Constr.rel_context * (Constr.rel_context * Constr.types) array) *
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index 674d7a2a91..8f06e1e4b8 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -414,11 +414,7 @@ exception UndefinableExpansion
     a substitution of the form [params, x : ind params] *)
 let compute_projections (kn, i as ind) mib =
   let pkt = mib.mind_packets.(i) in
-  let u = match mib.mind_universes with
-  | Monomorphic_ind _ -> Univ.Instance.empty
-  | Polymorphic_ind auctx -> Univ.make_abstract_instance auctx
-  | Cumulative_ind acumi -> Univ.make_abstract_instance (Univ.ACumulativityInfo.univ_context acumi)
-  in
+  let u = Univ.make_abstract_instance (Declareops.inductive_polymorphic_context mib) in
   let subst = List.init mib.mind_ntypes (fun i -> mkIndU ((kn, mib.mind_ntypes - i - 1), u)) in
   let rctx, _ = decompose_prod_assum (substl subst pkt.mind_nf_lc.(0)) in
   let ctx, paramslet = List.chop pkt.mind_consnrealdecls.(0) rctx in
@@ -471,7 +467,7 @@ let compute_projections (kn, i as ind) mib =
     Array.of_list (List.rev labs),
     Array.of_list (List.rev pbs)
 
-let build_inductive env names prv univs paramsctxt kn isrecord isfinite inds nmr recargs =
+let build_inductive env names prv univs variance 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
@@ -529,6 +525,7 @@ let build_inductive env names prv univs paramsctxt kn isrecord isfinite inds nmr
       mind_params_ctxt = paramsctxt;
       mind_packets = packets;
       mind_universes = univs;
+      mind_variance = variance;
       mind_private = prv;
       mind_typing_flags = Environ.typing_flags env;
     }
@@ -563,7 +560,7 @@ let build_inductive env names prv univs paramsctxt kn isrecord isfinite inds nmr
 
 let check_inductive env kn mie =
   (* First type-check the inductive definition *)
-  let (env_ar_par, univs, paramsctxt, inds) = IndTyping.typecheck_inductive env mie in
+  let (env_ar_par, univs, variance, paramsctxt, inds) = IndTyping.typecheck_inductive env mie in
   (* Then check positivity conditions *)
   let chkpos = (Environ.typing_flags env).check_guarded in
   let names = Array.map_of_list (fun entry -> entry.mind_entry_typename, entry.mind_entry_consnames)
@@ -574,6 +571,6 @@ let check_inductive env kn mie =
       (Array.map (fun ((_,lc),(indices,_),_) -> Context.Rel.nhyps indices,lc) inds)
   in
   (* Build the inductive packets *)
-    build_inductive env names mie.mind_entry_private univs
+    build_inductive env names mie.mind_entry_private univs variance
       paramsctxt kn mie.mind_entry_record mie.mind_entry_finite
       inds nmr recargs
diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index c62d0e7ded..848ae65c51 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -56,12 +56,7 @@ let inductive_paramdecls (mib,u) =
   Vars.subst_instance_context u mib.mind_params_ctxt
 
 let instantiate_inductive_constraints mib u =
-  let process auctx =  Univ.AUContext.instantiate 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)
-
+  Univ.AUContext.instantiate u (Declareops.inductive_polymorphic_context mib)
 
 (************************************************************************)
 
diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml
index f68dd158c2..421d932d9a 100644
--- a/kernel/mod_typing.ml
+++ b/kernel/mod_typing.ml
@@ -76,7 +76,7 @@ let rec check_with_def env struc (idl,(c,ctx)) mp equiv =
          as long as they have the right type *)
       let c', univs, ctx' =
         match cb.const_universes, ctx with
-        | Monomorphic_const _, None ->
+        | Monomorphic _, None ->
           let c',cst = match cb.const_body with
             | Undef _ | OpaqueDef _ ->
               let j = Typeops.infer env' c in
@@ -90,8 +90,8 @@ let rec check_with_def env struc (idl,(c,ctx)) mp equiv =
             | Primitive _ ->
               error_incorrect_with_constraint lab
           in
-          c', Monomorphic_const Univ.ContextSet.empty, cst
-        | Polymorphic_const uctx, Some ctx ->
+          c', Monomorphic Univ.ContextSet.empty, cst
+        | Polymorphic uctx, Some ctx ->
           let () =
             if not (UGraph.check_subtype (Environ.universes env) uctx ctx) then
               error_incorrect_with_constraint lab
@@ -114,7 +114,7 @@ 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;
-          c, Polymorphic_const ctx, Univ.Constraint.empty
+          c, Polymorphic ctx, Univ.Constraint.empty
         | _ -> error_incorrect_with_constraint lab
       in
       let def = Def (Mod_subst.from_val c') in
diff --git a/kernel/modops.ml b/kernel/modops.ml
index 1dc8eec0da..4f992d3972 100644
--- a/kernel/modops.ml
+++ b/kernel/modops.ml
@@ -50,6 +50,7 @@ type signature_mismatch_error =
   | IncompatibleUniverses of Univ.univ_inconsistency
   | IncompatiblePolymorphism of env * types * types
   | IncompatibleConstraints of { got : Univ.AUContext.t; expect : Univ.AUContext.t }
+  | IncompatibleVariance
 
 type module_typing_error =
   | SignatureMismatch of
@@ -325,11 +326,7 @@ let strengthen_const mp_from l cb resolver =
   |_ ->
     let kn = KerName.make mp_from l in
     let con = constant_of_delta_kn resolver kn in
-    let u =
-      match cb.const_universes with
-      | Monomorphic_const _ -> Univ.Instance.empty
-      | Polymorphic_const ctx -> Univ.make_abstract_instance ctx
-    in
+    let u = Univ.make_abstract_instance (Declareops.constant_polymorphic_context cb) in
       { cb with
         const_body = Def (Mod_subst.from_val (mkConstU (con,u)));
         const_private_poly_univs = None;
diff --git a/kernel/modops.mli b/kernel/modops.mli
index bb97f0171e..119ce2b359 100644
--- a/kernel/modops.mli
+++ b/kernel/modops.mli
@@ -111,6 +111,7 @@ type signature_mismatch_error =
   | IncompatibleUniverses of Univ.univ_inconsistency
   | IncompatiblePolymorphism of env * types * types
   | IncompatibleConstraints of { got : Univ.AUContext.t; expect : Univ.AUContext.t }
+  | IncompatibleVariance
 
 type module_typing_error =
   | SignatureMismatch of
diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml
index c32bdb85d6..df60899b95 100644
--- a/kernel/nativecode.ml
+++ b/kernel/nativecode.ml
@@ -1851,11 +1851,7 @@ and compile_named env sigma univ auxdefs id =
       Glet(Gnamed id, MLprimitive (Mk_var id))::auxdefs
 
 let compile_constant env sigma prefix ~interactive con cb =
-     let no_univs =
-       match cb.const_universes with
-       | Monomorphic_const _ -> true
-       | Polymorphic_const ctx -> Int.equal (Univ.AUContext.size ctx) 0
-     in
+    let no_univs = 0 = Univ.AUContext.size (Declareops.constant_polymorphic_context cb) in
     begin match cb.const_body with
     | Def t ->
       let t = Mod_subst.force_constr t in
diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index 61051c001d..b583d33e29 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -244,18 +244,14 @@ let inductive_cumulativity_arguments (mind,ind) =
   mind.Declarations.mind_packets.(ind).Declarations.mind_nrealargs
 
 let convert_inductives_gen cmp_instances cmp_cumul cv_pb (mind,ind) nargs u1 u2 s =
-  match mind.Declarations.mind_universes with
-  | Declarations.Monomorphic_ind _ ->
-    assert (Univ.Instance.length u1 = 0 && Univ.Instance.length u2 = 0);
-    s
-  | Declarations.Polymorphic_ind _ ->
-    cmp_instances u1 u2 s
-  | Declarations.Cumulative_ind cumi ->
+  match mind.Declarations.mind_variance with
+  | None -> cmp_instances u1 u2 s
+  | Some variances ->
     let num_param_arity = inductive_cumulativity_arguments (mind,ind) in
     if not (Int.equal num_param_arity nargs) then
       cmp_instances u1 u2 s
     else
-      cmp_cumul cv_pb (Univ.ACumulativityInfo.variance cumi) u1 u2 s
+      cmp_cumul cv_pb variances u1 u2 s
 
 let convert_inductives cv_pb ind nargs u1 u2 (s, check) =
   convert_inductives_gen (check.compare_instances ~flex:false) check.compare_cumul_instances
@@ -266,13 +262,9 @@ let constructor_cumulativity_arguments (mind, ind, ctor) =
   mind.Declarations.mind_packets.(ind).Declarations.mind_consnrealargs.(ctor - 1)
 
 let convert_constructors_gen cmp_instances cmp_cumul (mind, ind, cns) nargs u1 u2 s =
-  match mind.Declarations.mind_universes with
-  | Declarations.Monomorphic_ind _ ->
-    assert (Univ.Instance.length u1 = 0 && Univ.Instance.length u2 = 0);
-    s
-  | Declarations.Polymorphic_ind _ ->
-    cmp_instances u1 u2 s
-  | Declarations.Cumulative_ind _cumi ->
+  match mind.Declarations.mind_variance with
+  | None -> cmp_instances u1 u2 s
+  | Some _ ->
     let num_cnstr_args = constructor_cumulativity_arguments (mind,ind,cns) in
     if not (Int.equal num_cnstr_args nargs) then
       cmp_instances u1 u2 s
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 18a257047d..dc15d9d25e 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -312,8 +312,8 @@ let universes_of_private eff =
     | `Opaque (_, ctx) -> ctx :: acc
     in
     match eff.seff_body.const_universes with
-    | Monomorphic_const ctx -> ctx :: acc
-    | Polymorphic_const _ -> acc
+    | Monomorphic ctx -> ctx :: acc
+    | Polymorphic _ -> acc
   in
   List.fold_left fold [] (side_effects_of_private_constants eff)
 
@@ -465,7 +465,7 @@ let labels_of_mib mib =
 
 let globalize_constant_universes env cb =
   match cb.const_universes with
-  | Monomorphic_const cstrs ->
+  | Monomorphic cstrs ->
     Now (false, cstrs) ::
     (match cb.const_body with
      | (Undef _ | Def _ | Primitive _) -> []
@@ -476,15 +476,14 @@ let globalize_constant_universes env cb =
             match Future.peek_val fc with
              | None -> [Later fc]
              | Some c -> [Now (false, c)])
-  | Polymorphic_const _ ->
+  | Polymorphic _ ->
     [Now (true, Univ.ContextSet.empty)]
       
 let globalize_mind_universes mb =
   match mb.mind_universes with
-  | Monomorphic_ind ctx ->
+  | Monomorphic ctx ->
     [Now (false, ctx)]
-  | Polymorphic_ind _ -> [Now (true, Univ.ContextSet.empty)]
-  | Cumulative_ind _ -> [Now (true, Univ.ContextSet.empty)]
+  | Polymorphic _ -> [Now (true, Univ.ContextSet.empty)]
 
 let constraints_of_sfb env sfb = 
   match sfb with
@@ -612,13 +611,13 @@ let inline_side_effects env body side_eff =
       | _ -> assert false
       in
       match cb.const_universes with
-      | Monomorphic_const univs ->
+      | Monomorphic univs ->
         (** Abstract over the term at the top of the proof *)
         let ty = cb.const_type in
         let subst = Cmap_env.add c (Inr var) subst in
         let ctx = Univ.ContextSet.union ctx univs in
         (subst, var + 1, ctx, (cname c, b, ty, opaque) :: args)
-      | Polymorphic_const _ ->
+      | Polymorphic _ ->
         (** Inline the term to emulate universe polymorphism *)
         let subst = Cmap_env.add c (Inl b) subst in
         (subst, var, ctx, args)
@@ -700,10 +699,10 @@ let constant_entry_of_side_effect cb u =
   let open Entries in
   let univs =
     match cb.const_universes with
-    | Monomorphic_const uctx ->
-      Monomorphic_const_entry uctx
-    | Polymorphic_const auctx ->
-      Polymorphic_const_entry (Univ.AUContext.names auctx, Univ.AUContext.repr auctx)
+    | Monomorphic uctx ->
+      Monomorphic_entry uctx
+    | Polymorphic auctx ->
+      Polymorphic_entry (Univ.AUContext.names auctx, Univ.AUContext.repr auctx)
   in
   let pt =
     match cb.const_body, u with
@@ -756,8 +755,8 @@ let export_side_effects mb env c =
         let { seff_constant = kn; seff_body = cb ; _ } = eff in
         let env = Environ.add_constant kn cb env in
         match cb.const_universes with
-        | Polymorphic_const _ -> env
-        | Monomorphic_const ctx ->
+        | Polymorphic _ -> env
+        | Monomorphic ctx ->
           let ctx = match eff.seff_env with
           | `Nothing -> ctx
           | `Opaque(_, ctx') -> Univ.ContextSet.union ctx' ctx
diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml
index 2fc3aa99b5..dea72e8b59 100644
--- a/kernel/subtyping.ml
+++ b/kernel/subtyping.ml
@@ -92,11 +92,25 @@ let check_conv_error error why cst poly f env a1 a2 =
   with NotConvertible -> error why
      | Univ.UniverseInconsistency e -> error (IncompatibleUniverses e)
 
-let check_polymorphic_instance error env auctx1 auctx2 =
-  if not (UGraph.check_subtype (Environ.universes env) auctx2 auctx1) then
-    error (IncompatibleConstraints { got = auctx1; expect = auctx2; } )
-  else
-    Environ.push_context ~strict:false (Univ.AUContext.repr auctx2) env
+let check_universes error env u1 u2 =
+  match u1, u2 with
+  | Monomorphic _, Monomorphic _ -> env
+  | Polymorphic auctx1, Polymorphic auctx2 ->
+    if not (UGraph.check_subtype (Environ.universes env) auctx2 auctx1) then
+      error (IncompatibleConstraints { got = auctx1; expect = auctx2; } )
+    else
+      Environ.push_context ~strict:false (Univ.AUContext.repr auctx2) env
+  | Monomorphic _, Polymorphic _ -> error (PolymorphicStatusExpected true)
+  | Polymorphic _, Monomorphic _ -> error (PolymorphicStatusExpected false)
+
+let check_variance error v1 v2 =
+  match v1, v2 with
+  | None, None -> ()
+  | Some v1, Some v2 ->
+    if not (Array.for_all2 Variance.check_subtype v2 v1) then
+      error IncompatibleVariance
+  | None, Some _ -> error (CumulativeStatusExpected true)
+  | Some _, None -> error (CumulativeStatusExpected false)
 
 (* for now we do not allow reorderings *)
 
@@ -110,29 +124,9 @@ 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 env, inst =
-    match mib1.mind_universes, mib2.mind_universes with
-    | Monomorphic_ind _, Monomorphic_ind _ -> env, Univ.Instance.empty
-    | Polymorphic_ind auctx, Polymorphic_ind auctx' ->
-      let env = check_polymorphic_instance error env auctx auctx' in
-      env, Univ.make_abstract_instance auctx'
-    | Cumulative_ind cumi, Cumulative_ind cumi' ->
-      (** Currently there is no way to control variance of inductive types, but
-          just in case we require that they are in a subtyping relation. *)
-      let () =
-        let v = ACumulativityInfo.variance cumi in
-        let v' = ACumulativityInfo.variance cumi' in
-        if not (Array.for_all2 Variance.check_subtype v' v) then
-          CErrors.anomaly Pp.(str "Variance of " ++ KerName.print kn1 ++
-            str " is not compatible with the one of " ++ KerName.print kn2)
-      in
-      let auctx = Univ.ACumulativityInfo.univ_context cumi in
-      let auctx' = Univ.ACumulativityInfo.univ_context cumi' in
-      let env = check_polymorphic_instance error env auctx auctx' in
-      env, Univ.make_abstract_instance auctx'
-    | _ -> error 
-             (CumulativeStatusExpected (Declareops.inductive_is_cumulative mib2))
-  in
+  let env = check_universes error env mib1.mind_universes mib2.mind_universes in
+  let () = check_variance error mib1.mind_variance mib2.mind_variance in
+  let inst = make_abstract_instance (Declareops.inductive_polymorphic_context mib1) in
   let mib2 =  Declareops.subst_mind_body subst2 mib2 in
   let check_inductive_type cst name t1 t2 =
     check_conv (NotConvertibleInductiveField name)
@@ -235,17 +229,8 @@ let check_constant cst env l info1 cb2 spec2 subst1 subst2 =
       let cb1 = Declareops.subst_const_body subst1 cb1 in
       let cb2 = Declareops.subst_const_body subst2 cb2 in
       (* Start by checking universes *)
-      let poly, env =
-        match cb1.const_universes, cb2.const_universes with
-        | Monomorphic_const _, Monomorphic_const _ ->
-          false, env
-        | Polymorphic_const auctx1, Polymorphic_const auctx2 ->
-          true, check_polymorphic_instance error env auctx1 auctx2
-        | Monomorphic_const _, Polymorphic_const _ ->
-          error (PolymorphicStatusExpected true)
-        | Polymorphic_const _, Monomorphic_const _ ->
-          error (PolymorphicStatusExpected false)
-      in
+      let env = check_universes error env cb1.const_universes cb2.const_universes in
+      let poly = Declareops.constant_is_polymorphic cb1 in
       (* Now check types *)
       let typ1 = cb1.const_type in
       let typ2 = cb2.const_type in
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index 3cb5d17d34..929f1c13a3 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -65,23 +65,15 @@ let feedback_completion_typecheck =
   Option.iter (fun state_id ->
       Feedback.feedback ~id:state_id Feedback.Complete)
 
-let abstract_constant_universes = function
-  | Monomorphic_const_entry uctx ->
-    Univ.empty_level_subst, Monomorphic_const uctx
-  | Polymorphic_const_entry (nas, uctx) ->
-    let sbst, auctx = Univ.abstract_universes nas uctx in
-    let sbst = Univ.make_instance_subst sbst in
-    sbst, Polymorphic_const auctx
-
 let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) =
   match dcl with
     | ParameterEntry (ctx,(t,uctx),nl) ->
       let env = match uctx with
-        | Monomorphic_const_entry uctx -> push_context_set ~strict:true uctx env
-        | Polymorphic_const_entry (_, uctx) -> push_context ~strict:false uctx env
+        | Monomorphic_entry uctx -> push_context_set ~strict:true uctx env
+        | Polymorphic_entry (_, uctx) -> push_context ~strict:false uctx env
       in
       let j = infer env t in
-      let usubst, univs = abstract_constant_universes uctx in
+      let usubst, univs = Declareops.abstract_universes uctx in
       let c = Typeops.assumption_of_judgment env j in
       let t = Constr.hcons (Vars.subst_univs_level_constr usubst c) in
       {
@@ -115,7 +107,7 @@ let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) =
         | CPrimitives.OT_type _ -> Undef None in
       { Cooking.cook_body = cd;
         cook_type = ty;
-        cook_universes = Monomorphic_const uctxt;
+        cook_universes = Monomorphic uctxt;
         cook_private_univs = None;
         cook_inline = false;
         cook_context = None
@@ -134,7 +126,7 @@ the polymorphic case
   *)
   | DefinitionEntry ({ const_entry_type = Some typ;
                        const_entry_opaque = true;
-                       const_entry_universes = Monomorphic_const_entry univs; _ } as c) ->
+                       const_entry_universes = Monomorphic_entry univs; _ } as c) ->
       let env = push_context_set ~strict:true univs env in
       let { const_entry_body = body; const_entry_feedback = feedback_id ; _ } = c in
       let tyj = infer_type env typ in
@@ -165,7 +157,7 @@ the polymorphic case
       {
         Cooking.cook_body = def;
         cook_type = typ;
-        cook_universes = Monomorphic_const univs;
+        cook_universes = Monomorphic univs;
         cook_private_univs = None;
         cook_inline = c.const_entry_inline_code;
         cook_context = c.const_entry_secctx;
@@ -183,11 +175,11 @@ the polymorphic case
         body, Univ.ContextSet.union ctx ctx'
       in
       let env, usubst, univs, private_univs = match c.const_entry_universes with
-      | Monomorphic_const_entry univs ->
+      | Monomorphic_entry univs ->
         let ctx = Univ.ContextSet.union univs ctx in
         let env = push_context_set ~strict:true ctx env in
-        env, Univ.empty_level_subst, Monomorphic_const ctx, None
-      | Polymorphic_const_entry (nas, uctx) ->
+        env, Univ.empty_level_subst, Monomorphic ctx, None
+      | Polymorphic_entry (nas, uctx) ->
         (** [ctx] must contain local universes, such that it has no impact
             on the rest of the graph (up to transitivity). *)
         let env = push_context ~strict:false uctx env in
@@ -200,7 +192,7 @@ the polymorphic case
           if Univ.ContextSet.is_empty ctx then env, None
           else CErrors.anomaly Pp.(str "Local universes in non-opaque polymorphic definition.")
         in
-        env, sbst, Polymorphic_const auctx, local
+        env, sbst, Polymorphic auctx, local
       in
       let j = infer env body in
       let typ = match typ with
@@ -342,7 +334,7 @@ let translate_local_def env _id centry =
     const_entry_secctx = centry.secdef_secctx;
     const_entry_feedback = centry.secdef_feedback;
     const_entry_type = centry.secdef_type;
-    const_entry_universes = Monomorphic_const_entry Univ.ContextSet.empty;
+    const_entry_universes = Monomorphic_entry Univ.ContextSet.empty;
     const_entry_opaque = false;
     const_entry_inline_code = false;
   } in
@@ -360,8 +352,8 @@ let translate_local_def env _id centry =
        record_aux env ids_typ ids_def
   end;
   let () = match decl.cook_universes with
-  | Monomorphic_const ctx -> assert (Univ.ContextSet.is_empty ctx)
-  | Polymorphic_const _ -> assert false
+  | Monomorphic ctx -> assert (Univ.ContextSet.is_empty ctx)
+  | Polymorphic _ -> assert false
   in
   let c = match decl.cook_body with
   | Def c -> Mod_subst.force_constr c
diff --git a/kernel/univ.ml b/kernel/univ.ml
index 8940c0337e..09bf695915 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -989,68 +989,6 @@ let map_univ_abstracted f {univ_abstracted_value;univ_abstracted_binder} =
 
 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 an array of
-   Variance.t.
-
-    This data structure maintains the invariant that the variance
-   array has the same length as the universe instance. *)
-module CumulativityInfo =
-struct
-  type t = universe_context * Variance.t array
-
-  let make x =
-    if (Instance.length (UContext.instance (fst x))) =
-       (Array.length (snd x)) then x
-    else anomaly (Pp.str "Invalid subtyping information encountered!")
-
-  let empty = (UContext.empty, [||])
-  let is_empty (univs, variance) = UContext.is_empty univs && Array.is_empty variance
-
-  let pr prl (univs, variance) =
-    UContext.pr prl ~variance univs
-
-  let hcons (univs, variance) = (* should variance be hconsed? *)
-    (UContext.hcons univs, variance)
-
-  let univ_context (univs, _subtypcst) = univs
-  let variance (_univs, variance) = variance
-
-  (** This function takes a universe context representing constraints
-     of an inductive and produces a CumulativityInfo.t with the
-     trivial subtyping relation. *)
-  let from_universe_context univs =
-    (univs, Array.init (UContext.size univs) (fun _ -> Variance.Invariant))
-
-  let leq_constraints (_,variance) u u' csts = Variance.leq_constraints variance u u' csts
-  let eq_constraints (_,variance) u u' csts = Variance.eq_constraints variance u u' csts
-
-end
-
-let hcons_cumulativity_info = CumulativityInfo.hcons
-
-module ACumulativityInfo =
-struct
-  type t = AUContext.t * Variance.t array
-
-  let repr (auctx,var) = AUContext.repr auctx, var
-
-  let pr prl (univs, variance) =
-    AUContext.pr prl ~variance univs
-
-  let hcons (univs, variance) = (* should variance be hconsed? *)
-    (AUContext.hcons univs, variance)
-
-  let univ_context (univs, _subtypcst) = univs
-  let variance (_univs, variance) = variance
-
-  let leq_constraints (_,variance) u u' csts = Variance.leq_constraints variance u u' csts
-  let eq_constraints (_,variance) u u' csts = Variance.eq_constraints variance u u' csts
-end
-
-let hcons_abstract_cumulativity_info = ACumulativityInfo.hcons
-
 (** A set of universes with universe constraints.
     We linearize the set to a list after typechecking. 
     Beware, representation could change.
@@ -1211,10 +1149,6 @@ let abstract_universes nas ctx =
   let ctx = (nas, cstrs) in
   instance, ctx
 
-let abstract_cumulativity_info nas (univs, variance) =
-  let subst, univs = abstract_universes nas univs in
-  subst, (univs, variance)
-
 let rec compact_univ s vars i u =
   match u with
   | [] -> (s, List.rev vars)
@@ -1235,12 +1169,8 @@ let pr_constraints prl = Constraint.pr prl
 
 let pr_universe_context = UContext.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
 
 let pr_universe_subst = 
diff --git a/kernel/univ.mli b/kernel/univ.mli
index b83251e983..1fbebee350 100644
--- a/kernel/univ.mli
+++ b/kernel/univ.mli
@@ -368,45 +368,6 @@ type 'a univ_abstracted = {
 
 val map_univ_abstracted : ('a -> 'b) -> 'a univ_abstracted -> 'b univ_abstracted
 
-(** Universe info for cumulative inductive types: A context of
-   universe levels with universe constraints, representing local
-   universe variables and constraints, together with an array of
-   Variance.t.
-
-    This data structure maintains the invariant that the variance
-   array has the same length as the universe instance. *)
-module CumulativityInfo :
-sig
-  type t
-
-  val make : UContext.t * Variance.t array -> t
-
-  val empty : t
-  val is_empty : t -> bool
-
-  val univ_context : t -> UContext.t
-  val variance : t -> Variance.t array
-
-  (** This function takes a universe context representing constraints
-     of an inductive and produces a CumulativityInfo.t with the
-     trivial subtyping relation. *)
-  val from_universe_context : UContext.t -> t
-
-  val leq_constraints : t -> Instance.t constraint_function
-  val eq_constraints : t -> Instance.t constraint_function
-end
-
-module ACumulativityInfo :
-sig
-  type t
-
-  val repr : t -> CumulativityInfo.t
-  val univ_context : t -> AUContext.t
-  val variance : t -> Variance.t array
-  val leq_constraints : t -> Instance.t constraint_function
-  val eq_constraints : t -> Instance.t constraint_function
-end
-
 (** Universe contexts (as sets) *)
 
 (** A set of universes with universe Constraint.t.
@@ -487,7 +448,6 @@ val make_instance_subst : Instance.t -> universe_level_subst
 val make_inverse_instance_subst : Instance.t -> universe_level_subst
 
 val abstract_universes : Names.Name.t array -> UContext.t -> Instance.t * AUContext.t
-val abstract_cumulativity_info : Names.Name.t array -> CumulativityInfo.t -> Instance.t * ACumulativityInfo.t
 (** TODO: move universe abstraction out of the kernel *)
 
 val make_abstract_instance : AUContext.t -> Instance.t
@@ -505,10 +465,8 @@ val pr_constraint_type : constraint_type -> Pp.t
 val pr_constraints : (Level.t -> Pp.t) -> Constraint.t -> Pp.t
 val pr_universe_context : (Level.t -> Pp.t) -> ?variance:Variance.t array ->
   UContext.t -> Pp.t
-val pr_cumulativity_info : (Level.t -> Pp.t) -> CumulativityInfo.t -> Pp.t
 val pr_abstract_universe_context : (Level.t -> Pp.t) -> ?variance:Variance.t array ->
   AUContext.t -> Pp.t
-val pr_abstract_cumulativity_info : (Level.t -> Pp.t) -> ACumulativityInfo.t -> Pp.t
 val pr_universe_context_set : (Level.t -> Pp.t) -> ContextSet.t -> Pp.t
 val explain_universe_inconsistency : (Level.t -> Pp.t) ->
   univ_inconsistency -> Pp.t
@@ -524,5 +482,3 @@ val hcons_universe_set : LSet.t -> LSet.t
 val hcons_universe_context : UContext.t -> UContext.t
 val hcons_abstract_universe_context : AUContext.t -> AUContext.t
 val hcons_universe_context_set : ContextSet.t -> ContextSet.t
-val hcons_cumulativity_info : CumulativityInfo.t -> CumulativityInfo.t
-val hcons_abstract_cumulativity_info : ACumulativityInfo.t -> ACumulativityInfo.t
-- 
cgit v1.2.3