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

7 files changed, 273 insertions, 211 deletions

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 =