3 files changed, 6 insertions, 8 deletions
diff --git a/checker/indtypes.ml b/checker/indtypes.ml
index 50e65ef587..f6c510ee1c 100644
--- a/checker/indtypes.ml
+++ b/checker/indtypes.ml
@@ -531,10 +531,11 @@ let check_positivity env_ar mind params nrecp inds =
     Array.mapi (fun j t -> (Mrec(mind,j),t)) (Rtree.mk_rec_calls ntypes) in
   let lra_ind = List.rev (Array.to_list rc) in
   let lparams = rel_context_length params in
+  let ra_env =
+    List.init lparams (fun _ -> (Norec,mk_norec)) @ lra_ind in
+  let env_ar_par = push_rel_context params env_ar in
   let check_one i mip =
-    let ra_env =
-      List.init lparams (fun _ -> (Norec,mk_norec)) @ lra_ind in
-    let ienv = (env_ar, 1+lparams, ntypes, ra_env) in
+    let ienv = (env_ar_par, 1+lparams, ntypes, ra_env) in
       check_positivity_one ienv params nrecp (mind,i) mip.mind_nf_lc
   in
   let irecargs = Array.mapi check_one inds in
diff --git a/checker/inductive.ml b/checker/inductive.ml
index 5e34f04f51..269a98cb0e 100644
--- a/checker/inductive.ml
+++ b/checker/inductive.ml
@@ -388,7 +388,7 @@ let type_case_branches env (pind,largs) (p,pj) c =
 let check_case_info env indsp ci =
   let mib, mip as spec = lookup_mind_specif env indsp in
   if
-    not (eq_ind_chk indsp ci.ci_ind) ||
+    not (mind_equiv env indsp ci.ci_ind) ||
     (mib.mind_nparams <> ci.ci_npar) ||
     (mip.mind_consnrealdecls <> ci.ci_cstr_ndecls) ||
     (mip.mind_consnrealargs <> ci.ci_cstr_nargs) ||
diff --git a/checker/reduction.ml b/checker/reduction.ml
index 58a3f4e410..1158152f63 100644
--- a/checker/reduction.ml
+++ b/checker/reduction.ml
@@ -192,10 +192,7 @@ let convert_constructors
   | Monomorphic_ind _ | Polymorphic_ind _ -> convert_universes univs u1 u2
   | Cumulative_ind cumi ->
     let num_cnstr_args =
-      let nparamsctxt =
-        mind.mind_nparams + mind.mind_packets.(ind).mind_nrealargs
-      in
-      nparamsctxt + mind.mind_packets.(ind).mind_consnrealargs.(cns - 1)
+      mind.mind_nparams + mind.mind_packets.(ind).mind_consnrealargs.(cns - 1)
     in
     if not (num_cnstr_args = sv1 && num_cnstr_args = sv2) then
       convert_universes univs u1 u2