From 2e30531e78519a5b9c3773c2524e4fd4759cc5c8 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
Date: Thu, 1 Mar 2018 18:28:36 +0100
Subject: Delayed weak constraints for cumulative inductive types.

When comparing 2 irrelevant universes [u] and [v] we add a "weak
constraint" [UWeak(u,v)] to the UState. Then at minimization time a
weak constraint between unrelated universes where one is flexible
causes them to be unified.
---
 pretyping/unification.ml | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to 'pretyping/unification.ml')

diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 76bd88cc0..f2f922fd5 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -566,7 +566,8 @@ let force_eqs c =
   Constraints.fold
     (fun c acc ->
        let c' = match c with
-         | ULub (l, r) -> UEq (Univ.Universe.make l,Univ.Universe.make r)
+         (* Should we be forcing weak constraints? *)
+         | ULub (l, r) | UWeak (l, r) -> UEq (Univ.Universe.make l,Univ.Universe.make r)
          | ULe _ | UEq _ -> c
        in
         Constraints.add c' acc)
-- 
cgit v1.2.3