Merge PR #6128: Simplification: cumulativity information is variance information.

29 files changed, 635 insertions, 528 deletions

diff --git a/checker/indtypes.ml b/checker/indtypes.ml
index 4de597766..1807ae0ec 100644
--- a/checker/indtypes.ml
+++ b/checker/indtypes.ml
@@ -564,14 +564,23 @@ let check_subtyping cumi paramsctxt env inds =
       We must produce the substitution σ : [ Var(i) -> Var (i + n) | 0 <= i < n]
       and push the constraints [ Var(n) ... Var(2n - 1) |- cst{σ} ], together
       with the cumulativity constraints [ cumul_cst ]. *)
-  let len = AUContext.size (ACumulativityInfo.univ_context cumi) in
-  let inst = Instance.of_array (Array.init len (fun i -> Level.var (i + len))) in
+  let uctx = ACumulativityInfo.univ_context cumi in
+  let len = AUContext.size uctx in
+  let inst = Instance.of_array @@ Array.init len (fun i -> Level.var (i + len)) in
+
   let other_context = ACumulativityInfo.univ_context cumi in
   let uctx_other = UContext.make (inst, AUContext.instantiate inst other_context) in
-  let cumul_context = AUContext.repr (ACumulativityInfo.subtyp_context cumi) in
-  let cumul_cst = UContext.constraints cumul_context in
+  let cumul_cst =
+    Array.fold_left_i (fun i csts var ->
+        match var with
+        | Variance.Irrelevant -> csts
+        | Variance.Covariant -> Constraint.add (Level.var i,Le,Level.var (i+len)) csts
+        | Variance.Invariant -> Constraint.add (Level.var i,Eq,Level.var (i+len)) csts)
+      Constraint.empty (ACumulativityInfo.variance cumi)
+  in
   let env = Environ.push_context uctx_other env in
   let env = Environ.add_constraints cumul_cst env in
+
   (* process individual inductive types: *)
   Array.iter (fun { mind_user_lc = lc; mind_arity = arity } ->
       match arity with
diff --git a/checker/reduction.ml b/checker/reduction.ml
index 29bb8901e..2297c90b3 100644
--- a/checker/reduction.ml
+++ b/checker/reduction.ml
@@ -158,24 +158,17 @@ let compare_stacks f fmind lft1 stk1 lft2 stk2 =
 let convert_inductive_instances cv_pb cumi u u' univs =
   let len_instance =
       Univ.AUContext.size (Univ.ACumulativityInfo.univ_context cumi) in
-  let ind_subtypctx =  Univ.ACumulativityInfo.subtyp_context cumi in
   if not ((len_instance = Univ.Instance.length u) &&
           (len_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.AUContext.instantiate comp_subst ind_subtypctx
-    in
+    let variance = Univ.ACumulativityInfo.variance cumi in
     let comp_cst =
       match cv_pb with
-        CONV ->
-        let comp_cst' =
-          let comp_subst = (Univ.Instance.append u' u) in
-          Univ.AUContext.instantiate comp_subst ind_subtypctx
-        in
-        Univ.Constraint.union comp_cst comp_cst'
-      | CUMUL -> comp_cst
+      | CONV ->
+        Univ.Variance.eq_constraints variance u u' Univ.Constraint.empty
+      | CUMUL ->
+        Univ.Variance.leq_constraints variance u u' Univ.Constraint.empty
     in
     if (Univ.check_constraints comp_cst univs) then () else raise NotConvertible
 
diff --git a/checker/univ.ml b/checker/univ.ml
index 7d01657df..46b3ce680 100644
--- a/checker/univ.ml
+++ b/checker/univ.ml
@@ -1003,12 +1003,42 @@ end
 
 type abstract_universe_context = AUContext.t
 
+module Variance =
+struct
+  (** A universe position in the instance given to a cumulative
+     inductive can be the following. Note there is no Contravariant
+     case because [forall x : A, B <= forall x : A', B'] requires [A =
+     A'] as opposed to [A' <= A]. *)
+  type t = Irrelevant | Covariant | Invariant
+
+  let leq_constraint csts variance u u' =
+    match variance with
+    | Irrelevant -> csts
+    | Covariant -> Constraint.add (u, Le, u') csts
+    | Invariant -> Constraint.add (u, Eq, u') csts
+
+  let eq_constraint csts variance u u' =
+    match variance with
+    | Irrelevant -> csts
+    | Covariant | Invariant -> Constraint.add (u, Eq, u') csts
+
+  let leq_constraints variance u u' csts =
+    let len = Array.length u in
+    assert (len = Array.length u' && len = Array.length variance);
+    Array.fold_left3 leq_constraint csts variance u u'
+
+  let eq_constraints variance u u' csts =
+    let len = Array.length u in
+    assert (len = Array.length u' && len = Array.length variance);
+    Array.fold_left3 eq_constraint csts variance u u'
+end
+
 module CumulativityInfo =
 struct
-  type t = universe_context * universe_context
+  type t = universe_context * Variance.t array
 
   let univ_context (univcst, subtypcst) = univcst
-  let subtyp_context (univcst, subtypcst) = subtypcst
+  let variance (univs, variance) = variance
 
 end
 
diff --git a/checker/univ.mli b/checker/univ.mli
index 21c94d952..8c0685e0b 100644
--- a/checker/univ.mli
+++ b/checker/univ.mli
@@ -218,12 +218,25 @@ end
 
 type abstract_universe_context = AUContext.t
 
+module Variance :
+sig
+  (** A universe position in the instance given to a cumulative
+     inductive can be the following. Note there is no Contravariant
+     case because [forall x : A, B <= forall x : A', B'] requires [A =
+     A'] as opposed to [A' <= A]. *)
+  type t = Irrelevant | Covariant | Invariant
+
+  val leq_constraints : t array -> Instance.t constraint_function
+  val eq_constraints : t array -> Instance.t constraint_function
+end
+
+
 module ACumulativityInfo :
 sig
   type t
 
   val univ_context : t -> abstract_universe_context
-  val subtyp_context : t -> abstract_universe_context
+  val variance : t -> Variance.t array
 
 end
 
diff --git a/checker/values.ml b/checker/values.ml
index 313067cb6..55e1cdb6f 100644
--- a/checker/values.ml
+++ b/checker/values.ml
@@ -110,10 +110,12 @@ let v_cstrs =
        (v_tuple "univ_constraint"
           [|v_level;v_enum "order_request" 3;v_level|]))
 
+let v_variance = v_enum "variance" 3
+
 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_abs_cum_info = v_tuple "cumulativity_info" [|v_abs_context; Array v_variance|]
 let v_context_set = v_tuple "universe_context_set" [|v_hset v_level;v_cstrs|]
 
 (** kernel/term *)
diff --git a/doc/refman/Universes.tex b/doc/refman/Universes.tex
index a1a6a4391..6c84a1818 100644
--- a/doc/refman/Universes.tex
+++ b/doc/refman/Universes.tex
@@ -68,6 +68,13 @@ is only valid as long as \texttt{Top.4} is strictly smaller than
 monomorphic (not universe polymorphic), so the two universes
 (in this case \texttt{Top.3} and \texttt{Top.4}) are actually global levels.
 
+When printing \texttt{pidentity}, we can see the universes it binds in
+the annotation \texttt{@\{Top.2\}}. Additionally, when \texttt{Set
+  Printing Universes} is on we print the ``universe context'' of
+\texttt{pidentity} consisting of the bound universes and the
+constraints they must verify (for \texttt{pidentity} there are no
+constraints).
+
 Inductive types can also be declared universes polymorphic on universes
 appearing in their parameters or fields. A typical example is given by
 monoids:
@@ -138,7 +145,7 @@ producing global universe constraints, one can use the
 \optindex{Polymorphic Inductive Cumulativity}
 
 Polymorphic inductive types, coinductive types, variants and records can be
-declared cumulative using the \texttt{Cumulative}. Alternatively,
+declared cumulative using the \texttt{Cumulative} prefix. Alternatively,
 there is an option \texttt{Set Polymorphic Inductive Cumulativity} which when set,
 makes all subsequent \emph{polymorphic} inductive definitions cumulative.  When set,
 inductive types and the like can be enforced to be
@@ -151,15 +158,22 @@ Polymorphic Cumulative Inductive list {A : Type} :=
 \begin{coq_example}
 Print list.
 \end{coq_example}
-When printing \texttt{list}, the part of the output of the form
-\texttt{$\mathtt{\sim}$@\{i\} <= $\mathtt{\sim}$@\{j\} iff }
-indicates the universe constraints in order to have the subtyping
-$\WTEGLECONV{\mathtt{list@\{i\}} A}{\mathtt{list@\{j\}} B}$
-(for fully applied instances of \texttt{list}) whenever $\WTEGCONV{A}{B}$.
-In the case of \texttt{list} there is no constraint!
-This also means that any two instances of \texttt{list} are convertible:
-$\WTEGCONV{\mathtt{list@\{i\}} A}{\mathtt{list@\{j\}} B}$ whenever $\WTEGCONV{A}{B}$ and
-furthermore their corresponding (when fully applied to convertible arguments) constructors.
+When printing \texttt{list}, the universe context indicates the
+subtyping constraints by prefixing the level names with symbols.
+
+Because inductive subtypings are only produced by comparing inductives
+to themselves with universes changed, they amount to variance
+information: each universe is either invariant, covariant or
+irrelevant (there are no contravariant subtypings in Coq),
+respectively represented by the symbols \texttt{=}, \texttt{+} and
+\texttt{*}.
+
+Here we see that \texttt{list} binds an irrelevant universe, so any
+two instances of \texttt{list} are convertible:
+$\WTEGCONV{\mathtt{list@\{i\}} A}{\mathtt{list@\{j\}} B}$ whenever
+$\WTEGCONV{A}{B}$ and furthermore their corresponding (when fully
+applied to convertible arguments) constructors.
+
 See Chapter~\ref{Cic} for more details on convertibility and subtyping.
 The following is an example of a record with non-trivial subtyping relation:
 \begin{coq_example*}
@@ -168,8 +182,9 @@ Polymorphic Cumulative Record packType := {pk : Type}.
 \begin{coq_example}
 Print packType.
 \end{coq_example}
-Notice that as expected, \texttt{packType@\{i\}} and \texttt{packType@\{j\}} are
-convertible if and only if \texttt{i $=$ j}.
+\texttt{packType} binds a covariant universe, i.e.
+$\WTEGCONV{\mathtt{packType@\{i\}}}{\mathtt{packType@\{j\}}}$ whenever
+\texttt{i $\leq$ j}.
 
 Cumulative inductive types, coninductive types, variants and records
 only make sense when they are universe polymorphic. Therefore, an
diff --git a/engine/universes.ml b/engine/universes.ml
index eaddf98a8..3a00f0fd1 100644
--- a/engine/universes.ml
+++ b/engine/universes.ml
@@ -1103,14 +1103,3 @@ let solve_constraints_system levels level_bounds level_min =
     done;
   done;
   v
-
-
-(** Operations for universe_info_ind *)
-
-(** Given a universe context representing constraints of an inductive
-    this function produces a UInfoInd.t that with the trivial subtyping relation. *)
-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 CumulativityInfo.from_universe_context univcst freshunivs
diff --git a/engine/universes.mli b/engine/universes.mli
index 130dcf8bb..cb6e2ba1b 100644
--- a/engine/universes.mli
+++ b/engine/universes.mli
@@ -221,9 +221,3 @@ val pr_universe_opt_subst : universe_opt_subst -> Pp.t
 
 val solve_constraints_system : Universe.t option array -> Universe.t array -> Universe.t array ->
   Universe.t array
-
-(** Operations for universe_info_ind *)
-
-(** 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 : UContext.t -> CumulativityInfo.t
diff --git a/interp/declare.ml b/interp/declare.ml
index 55f825c25..72cdabfd2 100644
--- a/interp/declare.ml
+++ b/interp/declare.ml
@@ -364,13 +364,8 @@ let infer_inductive_subtyping (pth, mind_ent) =
   | Cumulative_ind_entry cumi ->
     begin
       let env = Global.env () in
-      let 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)
+        (pth, InferCumulativity.infer_inductive env mind_ent)
     end
 
 type inductive_obj = Dischargedhypsmap.discharged_hyps * mutual_inductive_entry
diff --git a/interp/discharge.ml b/interp/discharge.ml
index 75bfca307..710f88c3f 100644
--- a/interp/discharge.ml
+++ b/interp/discharge.ml
@@ -92,7 +92,7 @@ let process_inductive info modlist mib =
       let auctx = Univ.ACumulativityInfo.univ_context cumi in
       let subst, auctx = Lib.discharge_abstract_universe_context info auctx in
       let auctx = Univ.AUContext.repr auctx in
-      subst, Cumulative_ind_entry (Universes.univ_inf_ind_from_universe_context auctx)
+      subst, Cumulative_ind_entry (Univ.CumulativityInfo.from_universe_context auctx)
   in
   let discharge c = Vars.subst_univs_level_constr subst (expmod_constr modlist c) in
   let inds =
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index b117f8714..cfca335d3 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -234,22 +234,32 @@ let check_subtyping_arity_constructor env (subst : constr -> constr) (arcn : typ
 (* 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 = Context.Rel.nhyps paramsctxt in
-    let sbsubst = CumulativityInfo.subtyping_susbst cumi in
-    let dosubst = subst_univs_level_constr sbsubst 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 new_levels = Array.init (UContext.size uctx) (Level.make DirPath.empty) 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
+    in
+    let dosubst = 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 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 env = push_context (CumulativityInfo.subtyp_context cumi) env in
+    let subtyp_constraints =
+      CumulativityInfo.leq_constraints cumi
+        (UContext.instance uctx) instance_other
+        Constraint.empty
+    in
+    let env = Environ.add_constraints subtyp_constraints env in
     (* process individual inductive types: *)
     Array.iter (fun (id,cn,lc,(sign,arity)) ->
       match arity with
         | RegularArity (_, 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 _ -> ()
+        | TemplateArity _ ->
+          anomaly ~label:"check_subtyping"
+            Pp.(str "template polymorphism and cumulative polymorphism are not compatible")
     ) inds
 
 (* Type-check an inductive definition. Does not check positivity
diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index 6e42764a4..159d2ea66 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -200,13 +200,9 @@ let is_cumul = function CUMUL -> true | CONV -> false
 
 type 'a universe_compare = 
   { (* Might raise NotConvertible *)
-    compare : env -> conv_pb -> Sorts.t -> Sorts.t -> 'a -> 'a;
+    compare_sorts : env -> conv_pb -> Sorts.t -> Sorts.t -> 'a -> 'a;
     compare_instances: flex:bool -> Univ.Instance.t -> Univ.Instance.t -> 'a -> 'a;
-    conv_inductives : conv_pb -> (Declarations.mutual_inductive_body * int) -> Univ.Instance.t -> int ->
-      Univ.Instance.t -> int -> 'a -> 'a;
-    conv_constructors : (Declarations.mutual_inductive_body * int * int) ->
-      Univ.Instance.t -> int -> Univ.Instance.t -> int -> 'a -> 'a;
-  } 
+    compare_cumul_instances : Univ.Constraint.t -> 'a -> 'a }
 
 type 'a universe_state = 'a * 'a universe_compare
 
@@ -215,18 +211,68 @@ type ('a,'b) generic_conversion_function = env -> 'b universe_state -> 'a -> 'a
 type 'a infer_conversion_function = env -> UGraph.t -> 'a -> 'a -> Univ.Constraint.t
 
 let sort_cmp_universes env pb s0 s1 (u, check) =
-  (check.compare env pb s0 s1 u, check)
+  (check.compare_sorts env pb s0 s1 u, check)
 
 (* [flex] should be true for constants, false for inductive types and
    constructors. *)
 let convert_instances ~flex u u' (s, check) =
   (check.compare_instances ~flex u u' s, check)
-  
-let convert_inductives cv_pb ind u1 sv1 u2 sv2 (s, check) =
-  (check.conv_inductives cv_pb ind u1 sv1 u2 sv2 s, check)
 
-let convert_constructors cons u1 sv1 u2 sv2 (s, check) =
-  (check.conv_constructors cons u1 sv1 u2 sv2 s, check)
+let get_cumulativity_constraints cv_pb cumi u u' =
+  match cv_pb with
+  | CONV ->
+    Univ.ACumulativityInfo.eq_constraints cumi u u' Univ.Constraint.empty
+  | CUMUL ->
+    Univ.ACumulativityInfo.leq_constraints cumi u u' Univ.Constraint.empty
+
+let inductive_cumulativity_arguments (mind,ind) =
+  mind.Declarations.mind_nparams +
+  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 ->
+    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
+      let csts = get_cumulativity_constraints cv_pb cumi u1 u2 in
+      cmp_cumul csts s
+
+let convert_inductives cv_pb ind nargs u1 u2 (s, check) =
+  convert_inductives_gen (check.compare_instances ~flex:false) check.compare_cumul_instances
+    cv_pb ind nargs u1 u2 s, check
+
+let constructor_cumulativity_arguments (mind, ind, ctor) =
+  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.(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 ->
+    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
+    else
+      let csts = get_cumulativity_constraints CONV cumi u1 u2 in
+      cmp_cumul csts s
+
+let convert_constructors ctor nargs u1 u2 (s, check) =
+  convert_constructors_gen (check.compare_instances ~flex:false) check.compare_cumul_instances
+    ctor nargs u1 u2 s, check
 
 let conv_table_key infos k1 k2 cuniv =
   if k1 == k2 then cuniv else
@@ -518,15 +564,12 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv =
           convert_stacks l2r infos lft1 lft2 v1 v2 cuniv
         else
           let mind = Environ.lookup_mind (fst ind1) (info_env infos) in
-          let cuniv =
-            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
-          in
-          convert_stacks l2r infos lft1 lft2 v1 v2 cuniv
+          let nargs = CClosure.stack_args_size v1 in
+          if not (Int.equal nargs (CClosure.stack_args_size v2))
+          then raise NotConvertible
+          else
+            let cuniv = convert_inductives cv_pb (mind, snd ind1) nargs u1 u2 cuniv in
+            convert_stacks l2r infos lft1 lft2 v1 v2 cuniv
       else raise NotConvertible
 
     | (FConstruct ((ind1,j1),u1), FConstruct ((ind2,j2),u2)) ->
@@ -536,16 +579,12 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv =
           convert_stacks l2r infos lft1 lft2 v1 v2 cuniv
         else
           let mind = Environ.lookup_mind (fst ind1) (info_env infos) in
-          let cuniv =
-            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
-          in
-          convert_stacks l2r infos lft1 lft2 v1 v2 cuniv
+          let nargs = CClosure.stack_args_size v1 in
+          if not (Int.equal nargs (CClosure.stack_args_size v2))
+          then raise NotConvertible
+          else
+            let cuniv = convert_constructors (mind, snd ind1, j1) nargs u1 u2 cuniv in
+            convert_stacks l2r infos lft1 lft2 v1 v2 cuniv
       else raise NotConvertible
 	  
     (* Eta expansion of records *)
@@ -666,84 +705,14 @@ let check_convert_instances ~flex u u' univs =
   else raise NotConvertible
 
 (* general conversion and inference functions *)
-let infer_check_conv_inductives
-    infer_check_convert_instances
-    infer_check_inductive_instances
-    cv_pb (mind, ind) u1 sv1 u2 sv2 univs =
-  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
-      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 =
-  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
-        (* Context.Rel.length mind.Declarations.mind_params_ctxt *) in
-      nparamsctxt + mind.Declarations.mind_packets.(ind).Declarations.mind_consnrealargs.(cns - 1)
-    in
-    if not (num_cnstr_args = sv1 && num_cnstr_args = sv2) then
-      infer_check_convert_instances ~flex:false u1 u2 univs
-    else
-      infer_check_inductive_instances CONV cumi u1 u2 univs
-
-let check_inductive_instances cv_pb cumi u u' univs =
-  let length_ind_instance = 
-    Univ.AUContext.size (Univ.ACumulativityInfo.univ_context cumi)
-  in
-  let ind_subtypctx = Univ.ACumulativityInfo.subtyp_context cumi in
-  if not ((length_ind_instance = Univ.Instance.length u) &&
-          (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.AUContext.instantiate 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.AUContext.instantiate comp_subst ind_subtypctx
-        in
-        Univ.Constraint.union comp_cst comp_cst'
-      | CUMUL -> comp_cst
-    in
-    if (UGraph.check_constraints comp_cst univs) then univs
-    else raise NotConvertible
-
-let check_conv_inductives cv_pb ind u1 sv1 u2 sv2 univs =
-  infer_check_conv_inductives
-    check_convert_instances
-    check_inductive_instances
-    cv_pb ind u1 sv1 u2 sv2 univs
-
-let check_conv_constructors cns u1 sv1 u2 sv2 univs =
-  infer_check_conv_constructors
-    check_convert_instances
-    check_inductive_instances
-    cns u1 sv1 u2 sv2 univs
+let check_inductive_instances csts univs =
+  if (UGraph.check_constraints csts univs) then univs
+  else raise NotConvertible
 
 let checked_universes =
-  { compare = checked_sort_cmp_universes;
+  { compare_sorts = checked_sort_cmp_universes;
     compare_instances = check_convert_instances;
-    conv_inductives = check_conv_inductives;
-    conv_constructors = check_conv_constructors}
+    compare_cumul_instances = check_inductive_instances; }
 
 let infer_eq (univs, cstrs as cuniv) u u' =
   if UGraph.check_eq univs u u' then cuniv
@@ -786,49 +755,13 @@ 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 cumi u u' (univs, cstrs) =
-  let length_ind_instance = 
-    Univ.AUContext.size (Univ.ACumulativityInfo.univ_context cumi)
-  in
-  let ind_subtypctx =  Univ.ACumulativityInfo.subtyp_context cumi in
-  if not ((length_ind_instance = Univ.Instance.length u) &&
-          (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.AUContext.instantiate 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.AUContext.instantiate comp_subst ind_subtypctx
-        in
-        Univ.Constraint.union comp_cst comp_cst'
-      | CUMUL -> comp_cst
-    in
-    (univs, Univ.Constraint.union cstrs comp_cst)
-
-
-let infer_conv_inductives cv_pb ind u1 sv1 u2 sv2 univs =
-  infer_check_conv_inductives
-    infer_convert_instances
-    infer_inductive_instances
-    cv_pb ind u1 sv1 u2 sv2 univs
-
-let infer_conv_constructors cns u1 sv1 u2 sv2 univs =
-  infer_check_conv_constructors
-    infer_convert_instances
-    infer_inductive_instances
-    cns u1 sv1 u2 sv2 univs
-    
-let inferred_universes : (UGraph.t * Univ.Constraint.t) universe_compare = 
-  { compare = infer_cmp_universes;
+let infer_inductive_instances csts (univs,csts') =
+  (univs, Univ.Constraint.union csts csts')
+
+let inferred_universes : (UGraph.t * Univ.Constraint.t) universe_compare =
+  { compare_sorts = infer_cmp_universes;
     compare_instances = infer_convert_instances;
-    conv_inductives = infer_conv_inductives;
-    conv_constructors = infer_conv_constructors}
+    compare_cumul_instances = infer_inductive_instances; }
 
 let gen_conv cv_pb l2r reds env evars univs t1 t2 =
   let b = 
diff --git a/kernel/reduction.mli b/kernel/reduction.mli
index 573e4c8bd..0e6a2b819 100644
--- a/kernel/reduction.mli
+++ b/kernel/reduction.mli
@@ -35,15 +35,11 @@ type 'a extended_conversion_function =
 
 type conv_pb = CONV | CUMUL
 
-type 'a universe_compare = 
+type 'a universe_compare =
   { (* Might raise NotConvertible *)
-    compare : env -> conv_pb -> Sorts.t -> Sorts.t -> 'a -> 'a;
+    compare_sorts : env -> conv_pb -> Sorts.t -> Sorts.t -> 'a -> 'a;
     compare_instances: flex:bool -> Univ.Instance.t -> Univ.Instance.t -> 'a -> 'a;
-    conv_inductives : conv_pb -> (Declarations.mutual_inductive_body * int) -> Univ.Instance.t -> int ->
-      Univ.Instance.t -> int -> 'a -> 'a;
-    conv_constructors : (Declarations.mutual_inductive_body * int * int) ->
-      Univ.Instance.t -> int -> Univ.Instance.t -> int -> 'a -> 'a;
-  } 
+    compare_cumul_instances : Univ.Constraint.t -> 'a -> 'a }
 
 type 'a universe_state = 'a * 'a universe_compare
 
@@ -51,6 +47,12 @@ type ('a,'b) generic_conversion_function = env -> 'b universe_state -> 'a -> 'a
 
 type 'a infer_conversion_function = env -> UGraph.t -> 'a -> 'a -> Univ.Constraint.t
 
+val get_cumulativity_constraints : conv_pb -> Univ.ACumulativityInfo.t ->
+  Univ.Instance.t -> Univ.Instance.t -> Univ.Constraint.t
+
+val inductive_cumulativity_arguments : (Declarations.mutual_inductive_body * int) -> int
+val constructor_cumulativity_arguments : (Declarations.mutual_inductive_body * int * int) -> int
+
 val sort_cmp_universes : env -> conv_pb -> Sorts.t -> Sorts.t ->
   'a * 'a universe_compare -> 'a * 'a universe_compare
 
diff --git a/kernel/univ.ml b/kernel/univ.ml
index f72f6f26a..080bb7ad4 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -712,7 +712,48 @@ type universe_level_subst = universe_level universe_map
 (** A full substitution might involve algebraic universes *)
 type universe_subst = universe universe_map
 
-module Instance : sig 
+module Variance =
+struct
+  (** A universe position in the instance given to a cumulative
+     inductive can be the following. Note there is no Contravariant
+     case because [forall x : A, B <= forall x : A', B'] requires [A =
+     A'] as opposed to [A' <= A]. *)
+  type t = Irrelevant | Covariant | Invariant
+
+  let sup x y =
+    match x, y with
+    | Irrelevant, s | s, Irrelevant -> s
+    | Invariant, _ | _, Invariant -> Invariant
+    | Covariant, Covariant -> Covariant
+
+  let pr = function
+    | Irrelevant -> str "*"
+    | Covariant -> str "+"
+    | Invariant -> str "="
+
+  let leq_constraint csts variance u u' =
+    match variance with
+    | Irrelevant -> csts
+    | Covariant -> enforce_leq_level u u' csts
+    | Invariant -> enforce_eq_level u u' csts
+
+  let eq_constraint csts variance u u' =
+    match variance with
+    | Irrelevant -> csts
+    | Covariant | Invariant -> enforce_eq_level u u' csts
+
+  let leq_constraints variance u u' csts =
+    let len = Array.length u in
+    assert (len = Array.length u' && len = Array.length variance);
+    Array.fold_left3 leq_constraint csts variance u u'
+
+  let eq_constraints variance u u' csts =
+    let len = Array.length u in
+    assert (len = Array.length u' && len = Array.length variance);
+    Array.fold_left3 eq_constraint csts variance u u'
+end
+
+module Instance : sig
     type t = Level.t array
 
     val empty : t
@@ -732,7 +773,7 @@ module Instance : sig
 
     val subst_fn : universe_level_subst_fn -> t -> t
     
-    val pr : (Level.t -> Pp.t) -> t -> Pp.t
+    val pr : (Level.t -> Pp.t) -> ?variance:Variance.t array -> t -> Pp.t
     val levels : t -> LSet.t
 end = 
 struct
@@ -808,8 +849,12 @@ struct
 
   let levels x = LSet.of_array x
 
-  let pr =
-    prvect_with_sep spc
+  let pr prl ?variance =
+    let ppu i u =
+      let v = Option.map (fun v -> v.(i)) variance in
+      pr_opt_no_spc Variance.pr v ++ prl u
+    in
+    prvecti_with_sep spc ppu
 
   let equal t u = 
     t == u ||
@@ -873,9 +918,9 @@ struct
   let empty = (Instance.empty, Constraint.empty)
   let is_empty (univs, cst) = Instance.is_empty univs && Constraint.is_empty cst
 
-  let pr prl (univs, cst as ctx) =
+  let pr prl ?variance (univs, cst as ctx) =
     if is_empty ctx then mt() else
-      h 0 (Instance.pr prl univs ++ str " |= ") ++ h 0 (v 0 (Constraint.pr prl cst))
+      h 0 (Instance.pr prl ?variance univs ++ str " |= ") ++ h 0 (v 0 (Constraint.pr prl cst))
 
   let hcons (univs, cst) =
     (Instance.hcons univs, hcons_constraints cst)
@@ -911,66 +956,42 @@ end
 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
-    for inductive types.
+(** 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 context for
-    subtyping constraints is exactly twice as big as the context for
-    universe constraints. *)
+    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 * universe_context
+  type t = universe_context * Variance.t array
 
   let make x =
-    if (Instance.length (UContext.instance (snd x))) =
-       (Instance.length (UContext.instance (fst x))) * 2 then 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, UContext.empty)
-  let is_empty (univcst, subtypcst) = UContext.is_empty univcst && UContext.is_empty subtypcst
+  let empty = (UContext.empty, [||])
+  let is_empty (univs, variance) = UContext.is_empty univs && Array.is_empty variance
 
-  let halve_context ctx =
-    let len = Array.length (Instance.to_array ctx) in
-    let halflen = len / 2 in
-    (Instance.of_array (Array.sub (Instance.to_array ctx) 0 halflen),
-     Instance.of_array (Array.sub (Instance.to_array ctx) halflen halflen))
+  let pr prl (univs, variance) =
+    UContext.pr prl ~variance univs
 
-  let pr prl (univcst, subtypcst) =
-    if UContext.is_empty univcst then mt() else
-      let (ctx, ctx') = halve_context (UContext.instance subtypcst) in
-      (UContext.pr prl univcst) ++ fnl () ++ fnl () ++
-        h 0 (str "~@{" ++ Instance.pr prl ctx ++ str "} <= ~@{" ++ Instance.pr prl ctx' ++ str "} iff ")
-         ++ fnl () ++ h 0 (v 0 (Constraint.pr prl (UContext.constraints subtypcst)))
+  let hcons (univs, variance) = (* should variance be hconsed? *)
+    (UContext.hcons univs, variance)
 
-  let hcons (univcst, subtypcst) =
-    (UContext.hcons univcst, UContext.hcons subtypcst)
-
-  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 (Instance.to_array ctx)
+  let univ_context (univs, subtypcst) = univs
+  let variance (univs, variance) = variance
 
   (** This function takes a universe context representing constraints
-      of an inductive and a Instance.t of fresh universe names for the
-      subtyping (with the same length as the context in the given
-      universe context) and produces a UInfoInd.t that with the
-      trivial subtyping relation. *)
-  let from_universe_context univcst freshunivs =
-    let inst = (UContext.instance univcst) in
-    assert (Instance.length freshunivs = Instance.length inst);
-    (univcst, UContext.make (Instance.append inst freshunivs,
-                             create_trivial_subtyping inst freshunivs))
-
-  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'
+     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
 
@@ -1138,10 +1159,9 @@ let abstract_universes ctx =
   let ctx = UContext.make (instance, cstrs) in
   instance, ctx
 
-let abstract_cumulativity_info (univcst, substcst) = 
-  let instance, univcst = abstract_universes univcst in
-  let _, substcst = abstract_universes substcst in
-  (instance, (univcst, substcst))
+let abstract_cumulativity_info (univs, variance) =
+  let subst, univs = abstract_universes univs in
+  subst, (univs, variance)
 
 (** Pretty-printing *)
 
diff --git a/kernel/univ.mli b/kernel/univ.mli
index 63bef1b81..77ebf5a11 100644
--- a/kernel/univ.mli
+++ b/kernel/univ.mli
@@ -238,6 +238,20 @@ type universe_level_subst_fn = Level.t -> Level.t
 type universe_subst = Universe.t universe_map
 type universe_level_subst = Level.t universe_map
 
+module Variance :
+sig
+  (** A universe position in the instance given to a cumulative
+     inductive can be the following. Note there is no Contravariant
+     case because [forall x : A, B <= forall x : A', B'] requires [A =
+     A'] as opposed to [A' <= A]. *)
+  type t = Irrelevant | Covariant | Invariant
+
+  val sup : t -> t -> t
+
+  val pr : t -> Pp.t
+
+end
+
 (** {6 Universe instances} *)
 
 module Instance :
@@ -273,7 +287,7 @@ sig
   val subst_fn : universe_level_subst_fn -> t -> t
   (** Substitution by a level-to-level function. *)
 
-  val pr : (Level.t -> Pp.t) -> t -> Pp.t
+  val pr : (Level.t -> Pp.t) -> ?variance:Variance.t array -> t -> Pp.t
   (** Pretty-printing, no comments *)
 
   val levels : t -> LSet.t
@@ -347,36 +361,32 @@ end
 type abstract_universe_context = AUContext.t
 [@@ocaml.deprecated "Use AUContext.t"]
 
-(** Universe info for inductive types: A context of universe levels
-    with universe Constraint.t, representing local universe variables
-    and Constraint.t, together with a context of universe levels with
-    universe Constraint.t, representing conditions for subtyping used
-    for inductive types.
+(** 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 context for
-    subtyping Constraint.t is exactly twice as big as the context for
-    universe Constraint.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 * UContext.t -> t
+  val make : UContext.t * Variance.t array -> t
 
   val empty : t
   val is_empty : t -> bool
 
   val univ_context : t -> UContext.t
-  val subtyp_context : t -> UContext.t
-
-  (** This function takes a universe context representing Constraint.t
-      of an inductive and a Instance.t of fresh universe names for the
-      subtyping (with the same length as the context in the given
-      universe context) and produces a UInfoInd.t that with the
-      trivial subtyping relation. *)
-  val from_universe_context : UContext.t -> Instance.t -> t
+  val variance : t -> Variance.t array
 
-  val subtyping_susbst : t -> universe_level_subst
+  (** 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
 
 type cumulativity_info = CumulativityInfo.t
@@ -387,7 +397,9 @@ sig
   type t
 
   val univ_context : t -> AUContext.t
-  val subtyp_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
 
 type abstract_cumulativity_info = ACumulativityInfo.t
@@ -481,9 +493,11 @@ val make_abstract_instance : AUContext.t -> Instance.t
 
 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) -> UContext.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) -> AUContext.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) ->
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 41c4616f7..dc3acbc3e 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -353,19 +353,7 @@ let exact_ise_stack2 env evd f sk1 sk2 =
 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 length_ind_instance =
-    Univ.AUContext.size (Univ.ACumulativityInfo.univ_context cumi)
-  in
-  let ind_sbcst =  Univ.ACumulativityInfo.subtyp_context cumi in
-  if not ((length_ind_instance = Univ.Instance.length u) &&
-          (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.AUContext.instantiate comp_subst ind_sbcst in
-     Evd.add_constraints evd comp_cst
-    end
+  Evd.add_constraints evd (Reduction.get_cumulativity_constraints CUMUL cumi u u')
 
 let rec evar_conv_x ts env evd pbty term1 term2 =
   let term1 = whd_head_evar evd term1 in
diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml
index 78e6bc6f1..275a079d5 100644
--- a/pretyping/inductiveops.ml
+++ b/pretyping/inductiveops.ml
@@ -84,7 +84,7 @@ let mis_is_recursive_subset listind rarg =
     List.exists
       (fun ra ->
         match dest_recarg ra with
-	  | Mrec (_,i) -> Int.List.mem i listind
+          | Mrec (_,i) -> Int.List.mem i listind
           | _ -> false) rvec
   in
   Array.exists one_is_rec (dest_subterms rarg)
@@ -361,20 +361,20 @@ let make_case_or_project env sigma indf ci pred c branches =
        if (* dependent *) not (Vars.noccurn sigma 1 t) &&
           not (has_dependent_elim mib) then
        user_err ~hdr:"make_case_or_project"
-		    Pp.(str"Dependent case analysis not allowed" ++
-		     str" on inductive type " ++ Names.MutInd.print (fst ind))
+                    Pp.(str"Dependent case analysis not allowed" ++
+                     str" on inductive type " ++ Names.MutInd.print (fst ind))
      in
      let branch = branches.(0) in
      let ctx, br = decompose_lam_n_assum sigma (Array.length ps) branch in
      let n, subst =
        List.fold_right
          (fun decl (i, subst) ->
-	  match decl with
-	  | LocalAssum (na, t) ->
-	     let t = mkProj (Projection.make ps.(i) true, c) in
-	     (i + 1, t :: subst)
-	  | LocalDef (na, b, t) -> (i, Vars.substl subst b :: subst))
-	 ctx (0, [])
+          match decl with
+          | LocalAssum (na, t) ->
+             let t = mkProj (Projection.make ps.(i) true, c) in
+             (i + 1, t :: subst)
+          | LocalDef (na, b, t) -> (i, Vars.substl subst b :: subst))
+         ctx (0, [])
      in Vars.substl subst br
 
 (* substitution in a signature *)
@@ -511,25 +511,25 @@ let is_predicate_explicitly_dep env sigma pred arsign =
     let pv' = whd_all env sigma pval in
     match EConstr.kind sigma pv', arsign with
       | Lambda (na,t,b), (LocalAssum _)::arsign ->
-	  srec (push_rel_assum (na, t) env) b arsign
+          srec (push_rel_assum (na, t) env) b arsign
       | Lambda (na,_,t), _ ->
 
        (* The following code has an impact on the introduction names
-	  given by the tactics "case" and "inversion": when the
-	  elimination is not dependent, "case" uses Anonymous for
-	  inductive types in Prop and names created by mkProd_name for
-	  inductive types in Set/Type while "inversion" uses anonymous
-	  for inductive types both in Prop and Set/Type !!
-
-	  Previously, whether names were created or not relied on
-	  whether the predicate created in Indrec.make_case_com had a
-	  dependent arity or not. To avoid different predicates
-	  printed the same in v8, all predicates built in indrec.ml
-	  got a dependent arity (Aug 2004). The new way to decide
-	  whether names have to be created or not is to use an
-	  Anonymous or Named variable to enforce the expected
-	  dependency status (of course, Anonymous implies non
-	  dependent, but not conversely).
+          given by the tactics "case" and "inversion": when the
+          elimination is not dependent, "case" uses Anonymous for
+          inductive types in Prop and names created by mkProd_name for
+          inductive types in Set/Type while "inversion" uses anonymous
+          for inductive types both in Prop and Set/Type !!
+
+          Previously, whether names were created or not relied on
+          whether the predicate created in Indrec.make_case_com had a
+          dependent arity or not. To avoid different predicates
+          printed the same in v8, all predicates built in indrec.ml
+          got a dependent arity (Aug 2004). The new way to decide
+          whether names have to be created or not is to use an
+          Anonymous or Named variable to enforce the expected
+          dependency status (of course, Anonymous implies non
+          dependent, but not conversely).
 
           From Coq > 8.2, using or not the the effective dependency of
           the predicate is parametrable! *)
@@ -600,15 +600,15 @@ let rec instantiate_universes env evdref scl is = function
       let ctx,_ = Reduction.dest_arity env ty in
       let u = Univ.Universe.make l in
       let s =
-	(* Does the sort of parameter [u] appear in (or equal)
+        (* Does the sort of parameter [u] appear in (or equal)
            the sort of inductive [is] ? *)
         if univ_level_mem l is then
           scl (* constrained sort: replace by scl *)
         else
           (* unconstrained sort: replace by fresh universe *)
           let evm, s = Evd.new_sort_variable Evd.univ_flexible !evdref in
-	  let evm = Evd.set_leq_sort env evm s (Sorts.sort_of_univ u) in
-	    evdref := evm; s
+          let evm = Evd.set_leq_sort env evm s (Sorts.sort_of_univ u) in
+            evdref := evm; s
       in
       (LocalAssum (na,mkArity(ctx,s))) :: instantiate_universes env evdref scl is (sign, exp)
   | sign, [] -> sign (* Uniform parameters are exhausted *)
@@ -656,93 +656,3 @@ let control_only_guard env c =
     iter_constr_with_full_binders push_rel iter env c
   in
   iter env c
-
-(* inference of subtyping condition for inductive types *)
-
-let infer_inductive_subtyping_arity_constructor
-    (env, evd, csts) (subst : constr -> constr) (arcn : types) is_arity (params : Context.Rel.t) =
-  let numchecked = ref 0 in
-  let numparams = Context.Rel.nhyps params in
-  let update_contexts (env, evd, csts) csts' =
-    (Environ.add_constraints csts' env, Evd.add_constraints evd csts', Univ.Constraint.union csts csts')
-  in
-  let basic_check (env, evd, csts) tp =
-    let result =
-      if !numchecked >= numparams then
-        let csts' =
-          Reduction.infer_conv_leq ~evars:(Evd.existential_opt_value evd) env (Evd.universes evd) tp (subst tp)
-        in update_contexts (env, evd, csts) csts'
-      else
-        (env, evd, csts)
-    in
-    numchecked := !numchecked + 1; result
-  in
-  let infer_typ typ ctxs =
-   match typ with
-     | LocalAssum (_, typ') ->
-       begin
-         try
-           let (env, evd, csts) = basic_check ctxs typ' in (Environ.push_rel typ env, evd, csts)
-         with Reduction.NotConvertible -> 
-           anomaly ~label:"inference of record/inductive subtyping relation failed"
-             (Pp.str "Can't infer subtyping for record/inductive type")
-       end
-     | _ -> anomaly (Pp.str "")
-  in
-  let arcn' = Term.it_mkProd_or_LetIn arcn params in
-  let typs, codom = Reduction.dest_prod env arcn' in
-  let last_contexts = Context.Rel.fold_outside infer_typ typs ~init:(env, evd, csts) in
-  if not is_arity then basic_check last_contexts codom else last_contexts
-
-let infer_inductive_subtyping env evd mind_ent =
-  let { Entries.mind_entry_params = params;
-        Entries.mind_entry_inds = entries;
-        Entries.mind_entry_universes = ground_univs;
-      } = mind_ent
-  in
-  let 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/inductiveops.mli b/pretyping/inductiveops.mli
index 58b1ce6c3..55149552a 100644
--- a/pretyping/inductiveops.mli
+++ b/pretyping/inductiveops.mli
@@ -199,12 +199,3 @@ val type_of_inductive_knowing_conclusion :
 
 (********************)
 val control_only_guard : env -> types -> unit
-
-(* inference of subtyping condition for inductive types *)
-(* for debugging purposes only to be removed *)
-val infer_inductive_subtyping_arity_constructor : Environ.env * Evd.evar_map * Univ.Constraint.t ->
-(constr -> constr) ->
-types -> bool -> Context.Rel.t -> Environ.env * Evd.evar_map * Univ.Constraint.t
-
-val infer_inductive_subtyping : Environ.env -> Evd.evar_map -> Entries.mutual_inductive_entry ->
-  Entries.mutual_inductive_entry
diff --git a/pretyping/inferCumulativity.ml b/pretyping/inferCumulativity.ml
new file mode 100644
index 000000000..a0a8276c5
--- /dev/null
+++ b/pretyping/inferCumulativity.ml
@@ -0,0 +1,224 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+open Reduction
+open Declarations
+open Constr
+open Univ
+open Util
+
+(** Throughout this module we modify a map [variances] from local
+   universes to [Variance.t]. It starts as a trivial mapping to
+   [Irrelevant] and every time we encounter a local universe we
+   restrict it accordingly. *)
+
+let infer_level_eq u variances =
+  if LMap.mem u variances
+  then LMap.set u Variance.Invariant variances
+  else variances
+
+let infer_level_leq u variances =
+  match LMap.find u variances with
+  | exception Not_found -> variances
+  | varu -> LMap.set u (Variance.sup varu Variance.Covariant) variances
+
+let infer_generic_instance_eq variances u =
+  Array.fold_left (fun variances u -> infer_level_eq u variances)
+    variances (Instance.to_array u)
+
+let variance_pb cv_pb var =
+  let open Variance in
+  match cv_pb, var with
+  | _, Irrelevant -> Irrelevant
+  | _, Invariant -> Invariant
+  | CONV, Covariant -> Invariant
+  | CUMUL, Covariant -> Covariant
+
+let infer_cumulative_ind_instance cv_pb cumi variances u =
+  Array.fold_left2 (fun variances varu u ->
+      match LMap.find u variances with
+      | exception Not_found -> variances
+      | varu' ->
+        LMap.set u (Variance.sup varu' (variance_pb cv_pb varu)) variances)
+    variances (ACumulativityInfo.variance cumi) (Instance.to_array u)
+
+let infer_inductive_instance cv_pb env variances ind nargs u =
+  let mind = Environ.lookup_mind (fst ind) env in
+  match mind.mind_universes with
+  | Monomorphic_ind _ -> assert (Instance.is_empty u); variances
+  | Polymorphic_ind _ -> infer_generic_instance_eq variances u
+  | Cumulative_ind cumi ->
+    if not (Int.equal (inductive_cumulativity_arguments (mind,snd ind)) nargs)
+    then infer_generic_instance_eq variances u
+    else infer_cumulative_ind_instance cv_pb cumi variances u
+
+let infer_constructor_instance_eq env variances ((mi,ind),ctor) nargs u =
+  let mind = Environ.lookup_mind mi env in
+  match mind.mind_universes with
+  | Monomorphic_ind _ -> assert (Instance.is_empty u); variances
+  | Polymorphic_ind _ -> infer_generic_instance_eq variances u
+  | Cumulative_ind cumi ->
+    if not (Int.equal (constructor_cumulativity_arguments (mind,ind,ctor)) nargs)
+    then infer_generic_instance_eq variances u
+    else infer_cumulative_ind_instance CONV cumi variances u
+
+let infer_sort cv_pb variances s =
+  match cv_pb with
+  | CONV ->
+    LSet.fold infer_level_eq (Universe.levels (Sorts.univ_of_sort s)) variances
+  | CUMUL ->
+    LSet.fold infer_level_leq (Universe.levels (Sorts.univ_of_sort s)) variances
+
+let infer_table_key infos variances c =
+  let open Names in
+  match c with
+  | ConstKey (_, u) ->
+    infer_generic_instance_eq variances u
+  | VarKey _ | RelKey _ -> variances
+
+let rec infer_fterm cv_pb infos variances hd stk =
+  Control.check_for_interrupt ();
+  let open CClosure in
+  let hd,stk = whd_stack infos hd stk in
+  match fterm_of hd with
+  | FAtom a ->
+    begin match kind a with
+      | Sort s -> infer_sort cv_pb variances s
+      | Meta _ -> infer_stack infos variances stk
+      | _ -> assert false
+    end
+  | FEvar ((_,args),e) ->
+    let variances = infer_stack infos variances stk in
+    infer_vect infos variances (Array.map (mk_clos e) args)
+  | FRel _ -> variances
+  | FFlex fl ->
+    let variances = infer_table_key infos variances fl in
+    infer_stack infos variances stk
+  | FProj (_,c) ->
+    let variances = infer_fterm CONV infos variances c [] in
+    infer_stack infos variances stk
+  | FLambda _ ->
+    let (_,ty,bd) = destFLambda mk_clos hd in
+    let variances = infer_fterm CONV infos variances ty [] in
+    infer_fterm CONV infos variances bd []
+  | FProd (_,dom,codom) ->
+    let variances = infer_fterm CONV infos variances dom [] in
+    infer_fterm cv_pb infos variances codom []
+  | FInd (ind, u) ->
+    let variances =
+      if Instance.is_empty u then variances
+      else
+        let nargs = stack_args_size stk in
+        infer_inductive_instance cv_pb (info_env infos) variances ind nargs u
+    in
+    infer_stack infos variances stk
+  | FConstruct (ctor,u) ->
+    let variances =
+      if Instance.is_empty u then variances
+      else
+        let nargs = stack_args_size stk in
+        infer_constructor_instance_eq (info_env infos) variances ctor nargs u
+    in
+    infer_stack infos variances stk
+  | FFix ((_,(_,tys,cl)),e) | FCoFix ((_,(_,tys,cl)),e) ->
+    let n = Array.length cl in
+    let variances = infer_vect infos variances (Array.map (mk_clos e) tys) in
+    let le = Esubst.subs_liftn n e in
+    let variances = infer_vect infos variances (Array.map (mk_clos le) cl) in
+    infer_stack infos variances stk
+
+  (* Removed by whnf *)
+  | FLOCKED | FCaseT _ | FCast _ | FLetIn _ | FApp _ | FLIFT _ | FCLOS _ -> assert false
+
+and infer_stack infos variances (stk:CClosure.stack) =
+  match stk with
+  | [] -> variances
+  | z :: stk ->
+    let open CClosure in
+    let variances = match z with
+      | Zapp v -> infer_vect infos variances v
+      | Zproj _ -> variances
+      | Zfix (fx,a) ->
+        let variances = infer_fterm CONV infos variances fx [] in
+        infer_stack infos variances a
+      | ZcaseT (ci,p,br,e) ->
+        let variances = infer_fterm CONV infos variances (mk_clos e p) [] in
+        infer_vect infos variances (Array.map (mk_clos e) br)
+      | Zshift _ -> variances
+      | Zupdate _ -> variances
+    in
+    infer_stack infos variances stk
+
+and infer_vect infos variances v =
+  Array.fold_left (fun variances c -> infer_fterm CONV infos variances c []) variances v
+
+let infer_term cv_pb env variances c =
+  let open CClosure in
+  let reds = RedFlags.red_add_transparent betaiotazeta Names.full_transparent_state in
+  let infos = create_clos_infos reds env in
+  infer_fterm cv_pb infos variances (CClosure.inject c) []
+
+let infer_arity_constructor env variances arcn is_arity params =
+  let numchecked = ref 0 in
+  let numparams = Context.Rel.nhyps params in
+  let basic_check env variances tp =
+    let variances =
+      if !numchecked >= numparams then
+        infer_term CUMUL env variances tp
+      else
+        variances
+    in
+    numchecked := !numchecked + 1; variances
+  in
+  let infer_typ typ (env,variances) =
+    match typ with
+    | Context.Rel.Declaration.LocalAssum (_, typ') ->
+      (Environ.push_rel typ env, basic_check env variances typ')
+    | Context.Rel.Declaration.LocalDef _ -> assert false
+  in
+  let arcn' = Term.it_mkProd_or_LetIn arcn params in
+  let typs, codom = Reduction.dest_prod env arcn' in
+  let env, variances = Context.Rel.fold_outside infer_typ typs ~init:(env, variances) in
+  (* If we have Inductive foo@{i j} : ... -> Type@{i} := C : ... -> foo Type@{j}
+     i is irrelevant, j is invariant. *)
+  if not is_arity then basic_check env variances codom else variances
+
+let infer_inductive env mie =
+  let open Entries in
+  let { mind_entry_params = params;
+        mind_entry_inds = entries; } = mie
+  in
+  let univs =
+    match mie.mind_entry_universes with
+    | Monomorphic_ind_entry _
+    | Polymorphic_ind_entry _ as univs -> univs
+    | Cumulative_ind_entry cumi ->
+      let uctx = CumulativityInfo.univ_context cumi in
+      let uarray = Instance.to_array @@ UContext.instance uctx in
+      let env = Environ.push_context uctx env in
+      let variances =
+        Array.fold_left (fun variances u -> LMap.add u Variance.Irrelevant variances)
+          LMap.empty uarray
+      in
+      let variances = List.fold_left (fun variances entry ->
+          let _, params = Typeops.infer_local_decls env params in
+          let variances = infer_arity_constructor
+              env variances entry.mind_entry_arity true params
+          in
+          List.fold_left
+            (fun variances cons ->
+               infer_arity_constructor
+                 env variances cons false params)
+            variances entry.mind_entry_lc)
+          variances
+          entries
+      in
+      let variances = Array.map (fun u -> LMap.find u variances) uarray in
+      Cumulative_ind_entry (CumulativityInfo.make (uctx, variances))
+  in
+  { mie with mind_entry_universes = univs }
diff --git a/pretyping/inferCumulativity.mli b/pretyping/inferCumulativity.mli
new file mode 100644
index 000000000..a5037ea47
--- /dev/null
+++ b/pretyping/inferCumulativity.mli
@@ -0,0 +1,10 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+val infer_inductive : Environ.env -> Entries.mutual_inductive_entry ->
+  Entries.mutual_inductive_entry
diff --git a/pretyping/pretyping.mllib b/pretyping/pretyping.mllib
index 1da5b4567..ae4ad0be7 100644
--- a/pretyping/pretyping.mllib
+++ b/pretyping/pretyping.mllib
@@ -4,6 +4,7 @@ Locusops
 Pretype_errors
 Reductionops
 Inductiveops
+InferCumulativity
 Vnorm
 Arguments_renaming
 Nativenorm
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index 1893018a9..418ea271c 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -1324,79 +1324,17 @@ let sigma_compare_instances ~flex i0 i1 sigma =
      | Univ.UniverseInconsistency _ ->
 	raise Reduction.NotConvertible
 
-let sigma_check_inductive_instances cv_pb uinfind u u' sigma =
-  let len_instance =
-    Univ.AUContext.size (Univ.ACumulativityInfo.univ_context uinfind)
-  in
-  let ind_sbctx =  Univ.ACumulativityInfo.subtyp_context uinfind  in
-  if not ((len_instance = Univ.Instance.length u) &&
-          (len_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.AUContext.instantiate 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.AUContext.instantiate comp_subst ind_sbctx in
-        Univ.Constraint.union comp_cst comp_cst'
-      | Reduction.CUMUL -> comp_cst
-    in
-    try Evd.add_constraints sigma comp_cst
-    with Evd.UniversesDiffer
-       | Univ.UniverseInconsistency _ ->
-      raise Reduction.NotConvertible
-
-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 ->
-    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
-      in
-      if not (num_param_arity = sv1 && num_param_arity = sv2) then
-        raise Reduction.NotConvertible
-      else
-        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 ->
-    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
-        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
-        sigma_check_inductive_instances Reduction.CONV cumi u1 u2 sigma
+let sigma_check_inductive_instances csts sigma =
+  try Evd.add_constraints sigma csts
+  with Evd.UniversesDiffer
+     | Univ.UniverseInconsistency _ ->
+    raise Reduction.NotConvertible
 
 let sigma_univ_state = 
-  { Reduction.compare = sigma_compare_sorts;
-    Reduction.compare_instances = sigma_compare_instances;
-    Reduction.conv_inductives = sigma_conv_inductives;
-    Reduction.conv_constructors = sigma_conv_constructors}
+  let open Reduction in
+  { compare_sorts = sigma_compare_sorts;
+    compare_instances = sigma_compare_instances;
+    compare_cumul_instances = sigma_check_inductive_instances; }
 
 let infer_conv_gen conv_fun ?(catch_incon=true) ?(pb=Reduction.CUMUL)
     ?(ts=full_transparent_state) env sigma x y =
diff --git a/printing/prettyp.ml b/printing/prettyp.ml
index 2b7886d11..114a071ee 100644
--- a/printing/prettyp.ml
+++ b/printing/prettyp.ml
@@ -78,6 +78,15 @@ let print_ref reduce ref udecl =
       in EConstr.it_mkProd_or_LetIn ccl ctx
     else typ in
   let univs = Global.universes_of_global ref in
+  let variance = match ref with
+    | VarRef _ | ConstRef _ -> None
+    | IndRef (ind,_) | ConstructRef ((ind,_),_) ->
+      let mind = Environ.lookup_mind ind (Global.env ()) in
+      begin match mind.Declarations.mind_universes with
+        | Declarations.Monomorphic_ind _ | Declarations.Polymorphic_ind _ -> None
+        | Declarations.Cumulative_ind cumi -> Some (Univ.ACumulativityInfo.variance cumi)
+      end
+  in
   let inst = Univ.AUContext.instance univs in
   let univs = Univ.UContext.make (inst, Univ.AUContext.instantiate inst univs) in
   let env = Global.env () in
@@ -89,7 +98,7 @@ let print_ref reduce ref udecl =
     else mt ()
   in
   hov 0 (pr_global ref ++ inst ++ str " :" ++ spc () ++ pr_letype_env env sigma typ ++ 
-  	   Printer.pr_universe_ctx sigma univs)
+           Printer.pr_universe_ctx sigma ?variance univs)
 
 (********************************)
 (** Printing implicit arguments *)
diff --git a/printing/printer.ml b/printing/printer.ml
index a63004ceb..d720bc2f8 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -263,10 +263,10 @@ let pr_universe_ctx_set sigma c =
   else
     mt()
 
-let pr_universe_ctx sigma c =
+let pr_universe_ctx sigma ?variance c =
   if !Detyping.print_universes && not (Univ.UContext.is_empty c) then
     fnl()++pr_in_comment (fun c -> v 0 
-      (Univ.pr_universe_context (Termops.pr_evd_level sigma) c)) c
+      (Univ.pr_universe_context (Termops.pr_evd_level sigma) ?variance c)) c
   else
     mt()
 
diff --git a/printing/printer.mli b/printing/printer.mli
index 804014745..a3427920a 100644
--- a/printing/printer.mli
+++ b/printing/printer.mli
@@ -120,7 +120,8 @@ val pr_sort                : evar_map -> Sorts.t -> Pp.t
 val pr_polymorphic         : bool -> Pp.t
 val pr_cumulative          : bool -> bool -> Pp.t
 val pr_universe_instance   : evar_map -> Univ.UContext.t -> Pp.t
-val pr_universe_ctx        : evar_map -> Univ.UContext.t -> Pp.t
+val pr_universe_ctx        : evar_map -> ?variance:Univ.Variance.t array ->
+  Univ.UContext.t -> Pp.t
 val pr_universe_ctx_set    : evar_map -> Univ.ContextSet.t -> Pp.t
 val pr_constant_universes  : evar_map -> Entries.constant_universes_entry -> Pp.t
 val pr_cumulativity_info   : evar_map -> Univ.CumulativityInfo.t -> Pp.t
diff --git a/printing/printmod.ml b/printing/printmod.ml
index fb9d45a79..35487e09c 100644
--- a/printing/printmod.ml
+++ b/printing/printmod.ml
@@ -113,13 +113,12 @@ let print_one_inductive env sigma mib ((_,i) as ind) =
 let instantiate_cumulativity_info cumi =
   let open Univ in
   let univs = ACumulativityInfo.univ_context cumi in
-  let subtyp = ACumulativityInfo.subtyp_context cumi in
   let expose ctx =
     let inst = AUContext.instance ctx in
     let cst = AUContext.instantiate inst ctx in
     UContext.make (inst, cst)
   in
-  CumulativityInfo.make (expose univs, expose subtyp)
+  CumulativityInfo.make (expose univs, ACumulativityInfo.variance cumi)
 
 let print_mutual_inductive env mind mib udecl =
   let inds = List.init (Array.length mib.mind_packets) (fun x -> (mind, x))
diff --git a/test-suite/success/cumulativity.v b/test-suite/success/cumulativity.v
index 0ee85712e..1fb3abfe4 100644
--- a/test-suite/success/cumulativity.v
+++ b/test-suite/success/cumulativity.v
@@ -45,6 +45,15 @@ Section TpLift.
 
 End TpLift.
 
+Record Tp' := { tp' : Tp }.
+
+Definition CTp := Tp.
+(* here we have to reduce a constant to infer the correct subtyping. *)
+Record Tp'' := { tp'' : CTp }.
+
+Definition LiftTp'@{i j|i < j} : Tp'@{i} -> Tp'@{j} := fun x => x.
+Definition LiftTp''@{i j|i < j} : Tp''@{i} -> Tp''@{j} := fun x => x.
+
 Lemma LiftC_Lem (t : Tp) : LiftTp t = t.
 Proof. reflexivity. Qed.
 
@@ -98,3 +107,20 @@ Section down.
     intros H f g Hfg. exact (H f g Hfg).
   Defined.
 End down.
+
+Record Arrow@{i j} := { arrow : Type@{i} -> Type@{j} }.
+
+Fail Definition arrow_lift@{i i' j j' | i' < i, j < j'}
+  : Arrow@{i j} -> Arrow@{i' j'}
+  := fun x => x.
+
+Definition arrow_lift@{i i' j j' | i' = i, j < j'}
+  : Arrow@{i j} -> Arrow@{i' j'}
+  := fun x => x.
+
+Inductive Mut1 A :=
+| Base1 : Type -> Mut1 A
+| Node1 : (A -> Mut2 A) -> Mut1 A
+with Mut2 A :=
+     | Base2 : Type -> Mut2 A
+     | Node2 : Mut1 A -> Mut2 A.
diff --git a/vernac/comInductive.ml b/vernac/comInductive.ml
index 1c8677e9c..41474fc63 100644
--- a/vernac/comInductive.ml
+++ b/vernac/comInductive.ml
@@ -340,7 +340,7 @@ let interp_mutual_inductive (paramsl,indl) notations cum poly prv finite =
     match uctx with
     | Polymorphic_const_entry uctx ->
       if cum then
-        Cumulative_ind_entry (Universes.univ_inf_ind_from_universe_context uctx)
+        Cumulative_ind_entry (Univ.CumulativityInfo.from_universe_context uctx)
       else Polymorphic_ind_entry uctx
     | Monomorphic_const_entry uctx ->
       Monomorphic_ind_entry uctx
@@ -356,7 +356,7 @@ let interp_mutual_inductive (paramsl,indl) notations cum poly prv finite =
     }
   in
   (if poly && cum then
-      Inductiveops.infer_inductive_subtyping env_ar sigma mind_ent
+      InferCumulativity.infer_inductive env_ar mind_ent
    else mind_ent), Evd.universe_binders sigma, impls
 
 (* Very syntactical equality *)
diff --git a/vernac/record.ml b/vernac/record.ml
index 1e464eb8b..d9af5378f 100644
--- a/vernac/record.ml
+++ b/vernac/record.ml
@@ -423,16 +423,7 @@ let declare_structure finite ubinders univs id idbuild paramimpls params arity t
       mind_entry_universes = univs;
     }
   in
-  let mie =
-    match ctx with
-    | Polymorphic_const_entry ctx ->
-        let env = Global.env () in
-        let env' = Environ.push_context ctx env in
-        let evd = Evd.from_env env' in
-        Inductiveops.infer_inductive_subtyping env' evd mie
-    | Monomorphic_const_entry _ ->
-       mie
-  in
+  let mie = InferCumulativity.infer_inductive (Global.env ()) mie in
   let kn = ComInductive.declare_mutual_inductive_with_eliminations mie ubinders [(paramimpls,[])] in
   let rsp = (kn,0) in (* This is ind path of idstruc *)
   let cstr = (rsp,1) in
@@ -501,7 +492,7 @@ let declare_class finite def cum ubinders univs id idbuild paramimpls params ari
          match univs with
          | Polymorphic_const_entry univs ->
            if cum then
-             Cumulative_ind_entry (Universes.univ_inf_ind_from_universe_context univs)
+             Cumulative_ind_entry (Univ.CumulativityInfo.from_universe_context univs)
            else
              Polymorphic_ind_entry univs
          | Monomorphic_const_entry univs ->
@@ -632,7 +623,7 @@ let definition_structure (kind,cum,poly,finite,(is_coe,((loc,idstruc),pl)),ps,cf
         match univs with
         | Polymorphic_const_entry univs ->
           if cum then
-            Cumulative_ind_entry (Universes.univ_inf_ind_from_universe_context univs)
+            Cumulative_ind_entry (Univ.CumulativityInfo.from_universe_context univs)
           else
             Polymorphic_ind_entry univs
         | Monomorphic_const_entry univs ->