diff options
Diffstat (limited to 'kernel/cooking.ml')
| -rw-r--r-- | kernel/cooking.ml | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/kernel/cooking.ml b/kernel/cooking.ml index 88586352f6..22de9bfad5 100644 --- a/kernel/cooking.ml +++ b/kernel/cooking.ml @@ -157,7 +157,7 @@ type inline = bool type result = { cook_body : constr Mod_subst.substituted constant_def; cook_type : types; - cook_universes : constant_universes; + cook_universes : universes; cook_private_univs : Univ.ContextSet.t option; cook_inline : inline; cook_context : Constr.named_context option; @@ -185,10 +185,10 @@ let cook_constr { Opaqueproof.modlist ; abstract = (vars, subst, _) } c = let lift_univs cb subst auctx0 = match cb.const_universes with - | Monomorphic_const ctx -> + | Monomorphic ctx -> assert (AUContext.is_empty auctx0); - subst, (Monomorphic_const ctx) - | Polymorphic_const auctx -> + subst, (Monomorphic ctx) + | Polymorphic auctx -> (** Given a named instance [subst := uā ... uāāā] together with an abstract context [auctx0 := 0 ... n - 1 |= C{0, ..., n - 1}] of the same length, and another abstract context relative to the former context @@ -202,13 +202,13 @@ let lift_univs cb subst auctx0 = *) if (Univ.Instance.is_empty subst) then (** Still need to take the union for the constraints between globals *) - subst, (Polymorphic_const (AUContext.union auctx0 auctx)) + subst, (Polymorphic (AUContext.union auctx0 auctx)) else let ainst = Univ.make_abstract_instance auctx in let subst = Instance.append subst ainst in let substf = Univ.make_instance_subst subst in let auctx' = Univ.subst_univs_level_abstract_universe_context substf auctx in - subst, (Polymorphic_const (AUContext.union auctx0 auctx')) + subst, (Polymorphic (AUContext.union auctx0 auctx')) let cook_constant ~hcons { from = cb; info } = let { Opaqueproof.modlist; abstract } = info in |