From 4131f060ac42f121685817fcc9546c3899c09ab7 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sun, 31 Dec 2017 21:05:16 +0100 Subject: Add a comment about universe lifting in sections in the kernel. --- kernel/cooking.ml | 11 +++++++++++ 1 file changed, 11 insertions(+) (limited to 'kernel/cooking.ml') 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)) -- cgit v1.2.3