diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-12-31 21:05:16 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-12-31 21:06:33 +0100 |
| commit | 4131f060ac42f121685817fcc9546c3899c09ab7 (patch) | |
| tree | b3a2ef2b836bf7e7a9e3c963bac1f86fd0290375 /kernel/cooking.ml | |
| parent | bad3f3b784d3de8851615b8f4b7afba734232d8e (diff) | |
Add a comment about universe lifting in sections in the kernel.
Diffstat (limited to 'kernel/cooking.ml')
| -rw-r--r-- | kernel/cooking.ml | 11 |
1 files changed, 11 insertions, 0 deletions
diff --git a/kernel/cooking.ml b/kernel/cooking.ml index 1f407fc29..23a578d99 100644 --- a/kernel/cooking.ml +++ b/kernel/cooking.ml @@ -184,6 +184,17 @@ let lift_univs cb subst auctx0 = assert (AUContext.is_empty auctx0); subst, (Monomorphic_const ctx) | Polymorphic_const 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 + [auctx := 0 ... m - 1 |= C'{u₀, ..., uₙ₋₁, 0, ..., m - 1}], + construct the lifted abstract universe context + [0 ... n - 1 n ... n + m - 1 |= + C{0, ... n - 1} ∪ + C'{0, ..., n - 1, n, ..., n + m - 1} ] + together with the instance + [u₀ ... uₙ₋₁ Var(0) ... Var (m - 1)]. + *) 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)) |