From fd1f420aef96822bed2ce14214c34e41ceda9b4e Mon Sep 17 00:00:00 2001 From: Amin Timany Date: Sat, 1 Apr 2017 17:35:39 +0200 Subject: Using UInfoInd for universes in inductive types It stores both universe constraints and subtyping information for blocks of inductive declarations. At this stage the there is no inference or checking implemented. The subtyping information simply encodes equality of levels for the condition of subtyping. --- kernel/univ.ml | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) (limited to 'kernel/univ.ml') diff --git a/kernel/univ.ml b/kernel/univ.ml index e8b9ae33a..f124bb39e 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) -- cgit v1.2.3