From 9615c025a2a09b69f2001d44a66a1fddef74e680 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Thu, 29 Sep 2016 15:51:18 +0200
Subject: Fix bug #4869, allow Prop, Set, and level names in constraints.

---
 intf/vernacexpr.mli | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'intf')

diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli
index ed44704df4..e6599a30d1 100644
--- a/intf/vernacexpr.mli
+++ b/intf/vernacexpr.mli
@@ -346,7 +346,7 @@ type vernac_expr =
   | VernacScheme of (lident option * scheme) list
   | VernacCombinedScheme of lident * lident list
   | VernacUniverse of lident list
-  | VernacConstraint of (lident * Univ.constraint_type * lident) list
+  | VernacConstraint of (glob_level * Univ.constraint_type * glob_level) list
 
   (* Gallina extensions *)
   | VernacBeginSection of lident
-- 
cgit v1.2.3