From c8944dccb081c79eb47ca91c7e2cb5c50558aeaa Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau <matthieu.sozeau@inria.fr>
Date: Thu, 26 Feb 2015 13:13:05 +0100
Subject: Fix checker after addition of a universe context in with t := c
 constraints.

---
 checker/cic.mli | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'checker/cic.mli')

diff --git a/checker/cic.mli b/checker/cic.mli
index a793fefa8..90a0e9feb 100644
--- a/checker/cic.mli
+++ b/checker/cic.mli
@@ -333,7 +333,7 @@ type ('ty,'a) functorize =
 
 type with_declaration =
   | WithMod of Id.t list * module_path
-  | WithDef of Id.t list * constr
+  | WithDef of Id.t list * (constr * Univ.universe_context)
 
 type module_alg_expr =
   | MEident of module_path
-- 
cgit v1.2.3