diff options
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/declarations.ml | 4 | ||||
| -rw-r--r-- | kernel/declareops.ml | 7 | ||||
| -rw-r--r-- | kernel/entries.mli | 2 | ||||
| -rw-r--r-- | kernel/indtypes.ml | 14 | ||||
| -rw-r--r-- | kernel/inductive.ml | 2 | ||||
| -rw-r--r-- | kernel/safe_typing.ml | 2 | ||||
| -rw-r--r-- | kernel/term_typing.ml | 2 | ||||
| -rw-r--r-- | kernel/univ.ml | 8 | ||||
| -rw-r--r-- | kernel/vconv.ml | 2 |
9 files changed, 18 insertions, 25 deletions
diff --git a/kernel/declarations.ml b/kernel/declarations.ml index 9536407d38..1bb1e885f2 100644 --- a/kernel/declarations.ml +++ b/kernel/declarations.ml @@ -188,9 +188,7 @@ type mutual_inductive_body = { mind_polymorphic : bool; (** Is it polymorphic or not *) - mind_universes : Univ.universe_context; (** Local universe variables and constraints *) - - mind_subtyping : Univ.universe_context; (** Constraints for subtyping *) + mind_universes : Univ.universe_info_ind; (** Local universe variables and constraints together with subtyping constraints *) mind_private : bool option; (** allow pattern-matching: Some true ok, Some false blocked *) diff --git a/kernel/declareops.ml b/kernel/declareops.ml index 47a23c8555..cdea468adf 100644 --- a/kernel/declareops.ml +++ b/kernel/declareops.ml @@ -261,19 +261,18 @@ let subst_mind_body sub mib = mind_packets = Array.smartmap (subst_mind_packet sub) mib.mind_packets ; mind_polymorphic = mib.mind_polymorphic; mind_universes = mib.mind_universes; - mind_subtyping = mib.mind_subtyping; mind_private = mib.mind_private; mind_typing_flags = mib.mind_typing_flags; } let inductive_instance mib = if mib.mind_polymorphic then - Univ.UContext.instance mib.mind_universes + Univ.UContext.instance (Univ.UInfoInd.univ_context mib.mind_universes) else Univ.Instance.empty let inductive_context mib = if mib.mind_polymorphic then - Univ.instantiate_univ_context mib.mind_universes + Univ.instantiate_univ_context (Univ.UInfoInd.univ_context mib.mind_universes) else Univ.UContext.empty (** {6 Hash-consing of inductive declarations } *) @@ -306,7 +305,7 @@ let hcons_mind mib = { mib with mind_packets = Array.smartmap hcons_mind_packet mib.mind_packets; mind_params_ctxt = hcons_rel_context mib.mind_params_ctxt; - mind_universes = Univ.hcons_universe_context mib.mind_universes } + mind_universes = Univ.hcons_universe_info_ind mib.mind_universes } (** {6 Stm machinery } *) diff --git a/kernel/entries.mli b/kernel/entries.mli index 88584e3b3d..97c28025a4 100644 --- a/kernel/entries.mli +++ b/kernel/entries.mli @@ -50,7 +50,7 @@ type mutual_inductive_entry = { mind_entry_params : (Id.t * local_entry) list; mind_entry_inds : one_inductive_entry list; mind_entry_polymorphic : bool; - mind_entry_universes : Univ.universe_context * Univ.universe_context; + mind_entry_universes : Univ.universe_info_ind; (* universe constraints and the constraints for subtyping of inductive types in the block. *) mind_entry_private : bool option; diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml index 5d928facc7..94bf1a7704 100644 --- a/kernel/indtypes.ml +++ b/kernel/indtypes.ml @@ -220,7 +220,7 @@ let typecheck_inductive env mie = (* Check unicity of names *) mind_check_names mie; (* Params are typed-checked here *) - let env' = push_context (fst mie.mind_entry_universes) env in + let env' = push_context (Univ.UInfoInd.univ_context mie.mind_entry_universes) env in let (env_params,paramsctxt) = infer_local_decls env' mie.mind_entry_params in (* We first type arity of each inductive definition *) (* This allows building the environment of arities and to share *) @@ -822,10 +822,10 @@ let build_inductive env p prv ctx env_ar paramsctxt kn isrecord isfinite inds nm let hyps = used_section_variables env inds in let nparamargs = Context.Rel.nhyps paramsctxt in let nparamsctxt = Context.Rel.length paramsctxt in - let substunivs, ctxunivs = Univ.abstract_universes p (fst ctx) in - let substsbt, ctxsbt = Univ.abstract_universes p (snd ctx) in + let substunivs, ctxunivs = Univ.abstract_universes p (Univ.UInfoInd.univ_context ctx) in + let substsubtyp, ctxsubtyp = Univ.abstract_universes p (Univ.UInfoInd.subtyp_context ctx) in let paramsctxt = Vars.subst_univs_level_context substunivs paramsctxt in - let env_ar = + let env_ar = let ctxunivs = Environ.rel_context env_ar in let ctxunivs' = Vars.subst_univs_level_context substunivs ctxunivs in Environ.push_rel_context ctxunivs' env @@ -842,9 +842,6 @@ let build_inductive env p prv ctx env_ar paramsctxt kn isrecord isfinite inds nm let consnrealargs = Array.map (fun (d,_) -> Context.Rel.nhyps d - nparamargs) splayed_lc in - (* Check that the subtyping constraints (inferred outside kernel) - are valid. If so return (), otherwise raise an anomaly! *) - let () = () in (* Elimination sorts *) let arkind,kelim = match ar_kind with @@ -924,8 +921,7 @@ let build_inductive env p prv ctx env_ar paramsctxt kn isrecord isfinite inds nm mind_params_ctxt = paramsctxt; mind_packets = packets; mind_polymorphic = p; - mind_universes = ctxunivs; - mind_subtyping = ctxsbt; + mind_universes = Univ.UInfoInd.make (ctxunivs, ctxsubtyp); mind_private = prv; mind_typing_flags = Environ.typing_flags env; } diff --git a/kernel/inductive.ml b/kernel/inductive.ml index f3b03252db..0f0dc0d607 100644 --- a/kernel/inductive.ml +++ b/kernel/inductive.ml @@ -55,7 +55,7 @@ let inductive_paramdecls (mib,u) = let instantiate_inductive_constraints mib u = if mib.mind_polymorphic then - Univ.subst_instance_constraints u (Univ.UContext.constraints mib.mind_universes) + Univ.subst_instance_constraints u (Univ.UContext.constraints (Univ.UInfoInd.univ_context mib.mind_universes)) else Univ.Constraint.empty diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index f5e8e86530..1568fe0bf2 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -429,7 +429,7 @@ let globalize_mind_universes mb = if mb.mind_polymorphic then [Now (true, Univ.ContextSet.empty)] else - [Now (false, Univ.ContextSet.of_context mb.mind_universes)] + [Now (false, Univ.ContextSet.of_context (Univ.UInfoInd.univ_context mb.mind_universes))] let constraints_of_sfb env sfb = match sfb with diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml index bdfd00a8d3..3cf2299d83 100644 --- a/kernel/term_typing.ml +++ b/kernel/term_typing.ml @@ -313,7 +313,7 @@ let infer_declaration ~trust env kn dcl = in let term, typ = pb.proj_eta in Def (Mod_subst.from_val (hcons_constr term)), RegularArity typ, Some pb, - mib.mind_polymorphic, mib.mind_universes, false, None + mib.mind_polymorphic, Univ.UInfoInd.univ_context mib.mind_universes, false, None let global_vars_set_constant_type env = function | RegularArity t -> global_vars_set env t diff --git a/kernel/univ.ml b/kernel/univ.ml index e8b9ae33a0..f124bb39eb 100644 --- a/kernel/univ.ml +++ b/kernel/univ.ml @@ -1053,14 +1053,14 @@ struct let len = Array.length (Instance.to_array ctx) in let halflen = len / 2 in (Instance.of_array (Array.sub (Instance.to_array ctx) 0 halflen), - Instance.of_array (Array.sub (Instance.to_array ctx) halflen len)) + Instance.of_array (Array.sub (Instance.to_array ctx) halflen halflen)) let pr prl (univcst, subtypcst) = if UContext.is_empty univcst then mt() else let (ctx, ctx') = halve_context (UContext.instance subtypcst) in - (UContext.pr prl univcst) ++ - h 0 (str "~@{" ++ Instance.pr prl ctx ++ str "} <= ~@{" ++ Instance.pr prl ctx' ++ str "}") - ++ h 0 (v 0 (Constraint.pr prl (UContext.constraints subtypcst))) + (UContext.pr prl univcst) ++ fnl () ++ fnl () ++ + h 0 (str "~@{" ++ Instance.pr prl ctx ++ str "} <= ~@{" ++ Instance.pr prl ctx' ++ str "} iff ") + ++ fnl () ++ h 0 (v 0 (Constraint.pr prl (UContext.constraints subtypcst))) let hcons (univcst, subtypcst) = (UContext.hcons univcst, UContext.hcons subtypcst) diff --git a/kernel/vconv.ml b/kernel/vconv.ml index 74d956bef0..fa16622702 100644 --- a/kernel/vconv.ml +++ b/kernel/vconv.ml @@ -93,7 +93,7 @@ and conv_atom env pb k a1 stk1 a2 stk2 cu = if Environ.polymorphic_ind ind1 env then let mib = Environ.lookup_mind mi env in - let ulen = Univ.UContext.size mib.Declarations.mind_universes in + let ulen = Univ.UContext.size (Univ.UInfoInd.univ_context mib.Declarations.mind_universes) in match stk1 , stk2 with | [], [] -> assert (Int.equal ulen 0); cu | Zapp args1 :: stk1' , Zapp args2 :: stk2' -> |