diff options
| author | Gaëtan Gilbert | 2019-01-30 14:39:28 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2019-02-17 15:44:30 +0100 |
| commit | a9f0fd89cf3bb4b728eb451572a96f8599211380 (patch) | |
| tree | 577b7330af67793041cfaba8414005f93fc49c88 /kernel/cooking.ml | |
| parent | a49077ef67b8e70696ecacc311fc3070d1b7b461 (diff) | |
Separate variance and universe fields in inductives.
I think the usage looks cleaner this way.
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 |