Fix bugs

3 files changed, 34 insertions, 17 deletions

diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index eb8a0c85a0..ea22c3708f 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -494,7 +494,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
             if mind.Declarations.mind_polymorphic then
               begin
                 let num_param_arity =
-                  Context.Rel.length (mind.Declarations.mind_packets.(snd ind).Declarations.mind_arity_ctxt)
+                  mind.Declarations.mind_nparams + mind.Declarations.mind_packets.(snd ind).Declarations.mind_nrealargs
                 in
                 if not (num_param_arity = nparamsaplied && num_param_arity = nparamsaplied') then
                   UnifFailure (evd, NotSameHead)
@@ -520,7 +520,9 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
           if mind.Declarations.mind_polymorphic then
             begin
               let num_cnstr_args =
-                let nparamsctxt = Context.Rel.length mind.Declarations.mind_params_ctxt in
+                let nparamsctxt =
+                  mind.Declarations.mind_nparams + mind.Declarations.mind_packets.(snd ind).Declarations.mind_nrealargs
+                in
                 nparamsctxt + mind.Declarations.mind_packets.(snd ind).Declarations.mind_consnrealargs.(j - 1)
               in
               if not (num_cnstr_args = nparamsaplied && num_cnstr_args = nparamsaplied') then
diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml
index 1f8600dc2c..ebfb1f8a7c 100644
--- a/pretyping/inductiveops.ml
+++ b/pretyping/inductiveops.ml
@@ -659,14 +659,22 @@ let control_only_guard env c =
 (* inference of subtyping condition for inductive types *)
 
 let infer_inductive_subtyping_arity_constructor
-  (env, evd, csts) (subst : constr -> constr) (arcn : Term.types) is_arity =
+    (env, evd, csts) (subst : constr -> constr) (arcn : Term.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 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'
+    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
@@ -680,12 +688,14 @@ let infer_inductive_subtyping_arity_constructor
        end
      | _ -> anomaly (Pp.str "")
   in
-  let typs, codom = Reduction.dest_prod env arcn 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_inds = entries;
+  let { Entries.mind_entry_params = params;
+        Entries.mind_entry_inds = entries;
         Entries.mind_entry_polymorphic = poly;
         Entries.mind_entry_universes = ground_uinfind;
       } = mind_ent
@@ -704,15 +714,16 @@ let infer_inductive_subtyping env evd mind_ent =
       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 ctxs' = infer_inductive_subtyping_arity_constructor
-                          ctxs dosubst indentry.Entries.mind_entry_arity true
-            in
-            List.fold_left
-             (fun ctxs cons ->
-                infer_inductive_subtyping_arity_constructor ctxs dosubst cons false)
-             ctxs' indentry.Entries.mind_entry_lc
-         ) (env', evd', Univ.Constraint.empty) entries
+          (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 Univ.UInfoInd.make (Univ.UInfoInd.univ_context ground_uinfind,
            Univ.UContext.make
              (Univ.UContext.instance (Univ.UInfoInd.subtyp_context ground_uinfind),
diff --git a/pretyping/inductiveops.mli b/pretyping/inductiveops.mli
index 7d89b1b2bd..811f47f39a 100644
--- a/pretyping/inductiveops.mli
+++ b/pretyping/inductiveops.mli
@@ -201,6 +201,10 @@ 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 ->
+(Term.constr -> Term.constr) ->
+Term.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