From e03513b7309008a45957609739bcdaf3789f3052 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Thu, 12 Feb 2015 15:49:08 +0100
Subject: Fixing #3982 (conflict with max notation for universes).

---
 parsing/g_constr.ml4 | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4
index 8246df283b..3bb029a888 100644
--- a/parsing/g_constr.ml4
+++ b/parsing/g_constr.ml4
@@ -157,7 +157,7 @@ GEXTEND Gram
       ] ]
   ;
   universe:
-    [ [ "max("; ids = LIST1 ident SEP ","; ")" -> ids
+    [ [ IDENT "max"; "("; ids = LIST1 ident SEP ","; ")" -> ids
       | id = ident -> [id]
       ] ]
   ;
-- 
cgit v1.2.3