Fix bugs

1 files changed, 32 insertions, 29 deletions

diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index 15fe90835..a4c7a0573 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -215,20 +215,42 @@ let check_subtyping_arity_constructor env (subst : constr -> constr) (arcn : Ter
     numchecked := !numchecked + 1
   in
   let check_typ typ typ_env =
-   match typ with
-     | LocalAssum (_, typ') ->
-       begin
-         try 
-           basic_check env typ'; Environ.push_rel typ typ_env
-         with NotConvertible -> 
-           anomaly ~label:"bad inductive subtyping relation" (Pp.str "Invalid subtyping relation")
-       end
-     | _ -> anomaly (Pp.str "")
+    match typ with
+    | LocalAssum (_, typ') ->
+      begin
+       try
+          basic_check typ_env typ'; Environ.push_rel typ typ_env
+        with NotConvertible -> 
+          anomaly ~label:"bad inductive subtyping relation" (Pp.str "Invalid subtyping relation")
+      end
+    | _ -> anomaly (Pp.str "")
   in
   let typs, codom = dest_prod env arcn in
   let last_env = Context.Rel.fold_outside check_typ typs ~init:env in
   if not is_arity then basic_check last_env codom else ()
 
+(* Check that the subtyping information inferred for inductive types in the block is correct. *)
+(* This check produces a value of the unit type if successful or raises an anomaly if check fails. *)
+let check_subtyping mie paramsctxt env_ar inds = 
+    let numparams = Context.Rel.nhyps paramsctxt in
+    let sbsubst = UInfoInd.subtyping_susbst mie.mind_entry_universes in
+    let dosubst = subst_univs_level_constr sbsubst in
+    let uctx = UInfoInd.univ_context mie.mind_entry_universes 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_ar in
+    let env'' = Environ.push_context uctx_other env' in
+    let envsb = push_context (UInfoInd.subtyp_context mie.mind_entry_universes) env'' in
+    (* process individual inductive types: *)
+    Array.iter (fun (id,cn,lc,(sign,arity)) ->
+      match arity with
+        | RegularArity (_, full_arity, _) ->
+           check_subtyping_arity_constructor envsb dosubst full_arity numparams true;
+           Array.iter (fun cnt -> check_subtyping_arity_constructor envsb dosubst cnt numparams false) lc
+        | TemplateArity _ -> ()
+    ) inds
+
 (* Type-check an inductive definition. Does not check positivity
    conditions. *)
 (* TODO check that we don't overgeneralize construcors/inductive arities with
@@ -370,26 +392,7 @@ let typecheck_inductive env mie =
   in
   (* Check that the subtyping information inferred for inductive types in the block is correct. *)
   (* This check produces a value of the unit type if successful or raises an anomaly if check fails. *)
-  let () =
-    let numparams = List.length paramsctxt in
-    let sbsubst = UInfoInd.subtyping_susbst mie.mind_entry_universes in
-    let dosubst = subst_univs_level_constr sbsubst in
-    let uctx = UInfoInd.univ_context mie.mind_entry_universes 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_ar_par in
-    let env'' = Environ.push_context uctx_other env' in
-    let envsb = push_context (UInfoInd.subtyp_context mie.mind_entry_universes) env'' in
-    (* process individual inductive types: *)
-    Array.iter (fun (id,cn,lc,(sign,arity)) ->
-      match arity with
-        | RegularArity (_, full_arity, _) ->
-           check_subtyping_arity_constructor envsb dosubst full_arity numparams true;
-           Array.iter (fun cnt -> check_subtyping_arity_constructor envsb dosubst cnt numparams false) lc
-        | TemplateArity _ -> ()
-          (* TODO: When disabling template polumorphism raise anomaly if this constructor is not removed from the code base *)
-    ) inds
+  let () = check_subtyping mie paramsctxt env_arities inds
   in (env_arities, env_ar_par, paramsctxt, inds)
 
 (************************************************************************)