From 6461588b9fab2d59293b5c8380f0468421b5e0eb Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Wed, 27 Aug 2014 13:55:26 +0200
Subject: Fixing bug #3493.

Coq now accepts the [Universes u1 ... un] syntax.
---
 parsing/g_vernac.ml4 | 1 +
 1 file changed, 1 insertion(+)

diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 288263322d..013381382e 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -215,6 +215,7 @@ GEXTEND Gram
       | IDENT "Register"; IDENT "Inline"; id = identref ->
           VernacRegister(id, RegisterInline)
       | IDENT "Universe"; l = LIST1 identref -> VernacUniverse l
+      | IDENT "Universes"; l = LIST1 identref -> VernacUniverse l
       | IDENT "Constraint"; l = LIST1 univ_constraint SEP "," -> VernacConstraint l
   ] ]
   ;
-- 
cgit v1.2.3