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/declarations.mli | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'kernel/declarations.mli')

diff --git a/kernel/declarations.mli b/kernel/declarations.mli
index 561c66b422..7def963e73 100644
--- a/kernel/declarations.mli
+++ b/kernel/declarations.mli
@@ -246,8 +246,8 @@ and module_body =
     mod_type : module_signature; (** expanded type *)
     (** algebraic type, kept if it's relevant for extraction *)
     mod_type_alg : module_expression option;
-    (** set of all constraints in the module  *)
-    mod_constraints : Univ.constraints;
+    (** set of all universes constraints in the module  *)
+    mod_constraints : Univ.ContextSet.t;
     (** quotiented set of equivalent constants and inductive names *)
     mod_delta : Mod_subst.delta_resolver;
     mod_retroknowledge : Retroknowledge.action list }
-- 
cgit v1.2.3