From cc69a4697633e14fc00c9bd0858b38120645464b Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Wed, 23 Sep 2015 16:00:49 +0200
Subject: Univs: module constraints move to universe contexts as they might
 declare new universes (e.g. with).

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

(limited to 'kernel/mod_typing.mli')

diff --git a/kernel/mod_typing.mli b/kernel/mod_typing.mli
index b39e821254..80db12b0d3 100644
--- a/kernel/mod_typing.mli
+++ b/kernel/mod_typing.mli
@@ -30,7 +30,7 @@ val translate_modtype :
 *)
 
 type 'alg translation =
-  module_signature * 'alg option * delta_resolver * Univ.constraints
+  module_signature * 'alg option * delta_resolver * Univ.ContextSet.t
 
 val translate_mse :
   env -> module_path option -> inline -> module_struct_entry ->
-- 
cgit v1.2.3