Fix bugs

1 files changed, 26 insertions, 15 deletions

diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml
index 1f8600dc2..ebfb1f8a7 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),