Subtyping inference for inductoves and records

Also reinferred after sections discharge

1 files changed, 10 insertions, 60 deletions

diff --git a/vernac/command.ml b/vernac/command.ml
index b23eb9e6bf..35b75370e4 100644
--- a/vernac/command.ml
+++ b/vernac/command.ml
@@ -573,32 +573,6 @@ let check_param = function
 | CLocalAssum (nas, Generalized _, _) -> ()
 | CLocalPattern _ -> assert false
 
-let infer_inductive_subtyping_arity_constructor
-  (env, evd, csts) (subst : constr -> constr) (arcn : Term.types) is_arity =
-  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'
-  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 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 interp_mutual_inductive (paramsl,indl) notations poly prv finite =
   check_all_names_different indl;
   List.iter check_param paramsl;
@@ -676,41 +650,17 @@ let interp_mutual_inductive (paramsl,indl) notations poly prv finite =
 	  userimpls @ (lift_implicits len impls)) cimpls) indimpls constructors
   in
   let ground_uinfind = Universes.univ_inf_ind_from_universe_context uctx in
-  let uinfind =
-    let sbsubst = Univ.UInfoInd.subtyping_susbst ground_uinfind 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_ar_params 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 ctxs' = infer_inductive_subtyping_arity_constructor
-                        ctxs dosubst indentry.mind_entry_arity true
-          in
-          List.fold_left
-           (fun ctxs cons ->
-              infer_inductive_subtyping_arity_constructor ctxs dosubst cons false)
-           ctxs' indentry.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),
-             subtyp_constraints))
-  in
   (* Build the mutual inductive entry *)
-  { mind_entry_params = List.map prepare_param ctx_params;
-    mind_entry_record = None;
-    mind_entry_finite = finite;
-    mind_entry_inds = entries;
-    mind_entry_polymorphic = poly;
-    mind_entry_private = if prv then Some false else None;
-    mind_entry_universes = uinfind;
-  },
-    pl, impls
+  let mind_ent = 
+    { mind_entry_params = List.map prepare_param ctx_params;
+      mind_entry_record = None;
+      mind_entry_finite = finite;
+      mind_entry_inds = entries;
+      mind_entry_polymorphic = poly;
+      mind_entry_private = if prv then Some false else None;
+      mind_entry_universes = ground_uinfind;
+    }
+  in (Inductiveops.infer_inductive_subtyping env_ar_params evd mind_ent), pl, impls
 
 (* Very syntactical equality *)
 let eq_local_binders bl1 bl2 =