From 253d8c7cfd878912512f31d6aa09931959b66041 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Sat, 21 Feb 2015 19:03:12 +0100
Subject: Import (module): Do not force constraints if not ready (Close #4066)

---
 kernel/safe_typing.ml | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

(limited to 'kernel')

diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 20cecc84a6..65d1de7e11 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -379,7 +379,9 @@ let globalize_constant_universes env cb =
 	  | None -> []
 	  | Some fc ->
             match Future.peek_val fc with
-            | None -> [Later (Future.chain ~pure:true fc Univ.ContextSet.constraints)]
+            | None -> [Later (Future.chain
+                 ~greedy:(not (Future.is_exn fc))
+                 ~pure:true fc Univ.ContextSet.constraints)]
             | Some c -> [Now (Univ.ContextSet.constraints c)])
       
 let globalize_mind_universes mb =
-- 
cgit v1.2.3