diff options
-rw-r--r-- | interp/declare.ml | 7 | ||||
-rw-r--r-- | pretyping/inductiveops.ml | 29 | ||||
-rw-r--r-- | pretyping/inductiveops.mli | 7 | ||||
-rw-r--r-- | vernac/comInductive.ml | 2 | ||||
-rw-r--r-- | vernac/record.ml | 11 |
5 files changed, 17 insertions, 39 deletions
diff --git a/interp/declare.ml b/interp/declare.ml index 55f825c25..0bfc9060b 100644 --- a/interp/declare.ml +++ b/interp/declare.ml @@ -364,13 +364,8 @@ let infer_inductive_subtyping (pth, mind_ent) = | Cumulative_ind_entry cumi -> begin let env = Global.env () in - let env' = - Environ.push_context - (Univ.CumulativityInfo.univ_context cumi) env - in (* let (env'', typed_params) = Typeops.infer_local_decls env' (mind_ent.mind_entry_params) in *) - let evd = Evd.from_env env' in - (pth, Inductiveops.infer_inductive_subtyping env' evd mind_ent) + (pth, Inductiveops.infer_inductive_subtyping env mind_ent) end type inductive_obj = Dischargedhypsmap.discharged_hyps * mutual_inductive_entry diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml index df0b53e9c..23a4ade3f 100644 --- a/pretyping/inductiveops.ml +++ b/pretyping/inductiveops.ml @@ -660,20 +660,20 @@ 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 : types) is_arity (params : Context.Rel.t) = + (env, csts) (subst : constr -> constr) (arcn : 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') + let update_contexts (env, csts) csts' = + (Environ.add_constraints csts' env, Univ.Constraint.union csts csts') in - let basic_check (env, evd, csts) tp = + let basic_check (env, csts) tp = 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' + Reduction.infer_conv_leq env (Environ.universes env) tp (subst tp) + in update_contexts (env, csts) csts' else - (env, evd, csts) + (env, csts) in numchecked := !numchecked + 1; result in @@ -682,7 +682,7 @@ let infer_inductive_subtyping_arity_constructor | LocalAssum (_, typ') -> begin try - let (env, evd, csts) = basic_check ctxs typ' in (Environ.push_rel typ env, evd, csts) + let (env, csts) = basic_check ctxs typ' in (Environ.push_rel typ env, csts) with Reduction.NotConvertible -> anomaly ~label:"inference of record/inductive subtyping relation failed" (Pp.str "Can't infer subtyping for record/inductive type") @@ -691,7 +691,7 @@ let infer_inductive_subtyping_arity_constructor 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 + let last_contexts = Context.Rel.fold_outside infer_typ typs ~init:(env, csts) in if not is_arity then basic_check last_contexts codom else last_contexts type ukind = @@ -731,7 +731,7 @@ let make_variance uctx lmap csts = ) csts; variance -let infer_inductive_subtyping env evd mind_ent = +let infer_inductive_subtyping env mind_ent = let { Entries.mind_entry_params = params; Entries.mind_entry_inds = entries; Entries.mind_entry_universes = ground_univs; @@ -744,6 +744,7 @@ let infer_inductive_subtyping env evd mind_ent = | Entries.Cumulative_ind_entry cumi -> begin let uctx = CumulativityInfo.univ_context cumi in + let env = Environ.push_context uctx env in let new_levels = Array.init (UContext.size uctx) (Level.make DirPath.empty) in let lmap = Array.fold_left2 (fun lmap u u' -> LMap.add u u' lmap) LMap.empty (Instance.to_array @@ UContext.instance uctx) new_levels @@ -757,11 +758,7 @@ let infer_inductive_subtyping env evd mind_ent = let uctx_other = Univ.UContext.make (instance_other, constraints_other) in let env = Environ.push_context uctx env in let env = Environ.push_context uctx_other env in - let evd = - Evd.merge_context_set UState.UnivRigid - evd (Univ.ContextSet.of_context uctx_other) - in - let (_, _, subtyp_constraints) = + let (_, subtyp_constraints) = List.fold_left (fun ctxs indentry -> let _, params = Typeops.infer_local_decls env params in @@ -774,7 +771,7 @@ let infer_inductive_subtyping env evd mind_ent = ctxs dosubst cons false params ) ctxs' indentry.Entries.mind_entry_lc - ) (env, evd, Univ.Constraint.empty) entries + ) (env, Univ.Constraint.empty) entries in let variance = make_variance uctx lmap subtyp_constraints in Entries.Cumulative_ind_entry diff --git a/pretyping/inductiveops.mli b/pretyping/inductiveops.mli index 58b1ce6c3..f6b11ee66 100644 --- a/pretyping/inductiveops.mli +++ b/pretyping/inductiveops.mli @@ -201,10 +201,5 @@ 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 -> -(constr -> constr) -> -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 -> +val infer_inductive_subtyping : Environ.env -> Entries.mutual_inductive_entry -> Entries.mutual_inductive_entry diff --git a/vernac/comInductive.ml b/vernac/comInductive.ml index 3f8d413b7..faac16802 100644 --- a/vernac/comInductive.ml +++ b/vernac/comInductive.ml @@ -356,7 +356,7 @@ let interp_mutual_inductive (paramsl,indl) notations cum poly prv finite = } in (if poly && cum then - Inductiveops.infer_inductive_subtyping env_ar sigma mind_ent + Inductiveops.infer_inductive_subtyping env_ar mind_ent else mind_ent), Evd.universe_binders sigma, impls (* Very syntactical equality *) diff --git a/vernac/record.ml b/vernac/record.ml index 31c0483b4..6e35ac4db 100644 --- a/vernac/record.ml +++ b/vernac/record.ml @@ -423,16 +423,7 @@ let declare_structure finite ubinders univs id idbuild paramimpls params arity t mind_entry_universes = univs; } in - let mie = - match ctx with - | Polymorphic_const_entry ctx -> - let env = Global.env () in - let env' = Environ.push_context ctx env in - let evd = Evd.from_env env' in - Inductiveops.infer_inductive_subtyping env' evd mie - | Monomorphic_const_entry _ -> - mie - in + let mie = Inductiveops.infer_inductive_subtyping (Global.env ()) mie in let kn = ComInductive.declare_mutual_inductive_with_eliminations mie ubinders [(paramimpls,[])] in let rsp = (kn,0) in (* This is ind path of idstruc *) let cstr = (rsp,1) in |