From 62fb849cf9410ddc2d9f355570f4fb859f3044c3 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau <mattam@mattam.org>
Date: Tue, 25 Mar 2014 18:29:28 +0100
Subject: Adapt universe polymorphic branch to new handling of futures for
 delayed proofs.

---
 kernel/safe_typing.mli | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'kernel/safe_typing.mli')

diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli
index ad2148ead..5b5457c38 100644
--- a/kernel/safe_typing.mli
+++ b/kernel/safe_typing.mli
@@ -140,7 +140,7 @@ val export :
     module_path * compiled_library * native_library
 
 (* Constraints are non empty iff the file is a vi2vo *)
-val import : compiled_library -> Univ.constraints -> vodigest ->
+val import : compiled_library -> Univ.universe_context -> vodigest ->
   (module_path * Nativecode.symbol array) safe_transformer
 
 (** {6 Safe typing judgments } *)
-- 
cgit v1.2.3