From d9e54d65cc808eab2908beb7a7a2c96005118ace Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Mon, 12 Jun 2017 17:47:51 +0200
Subject: Allow declaring universe binders with no constraints with @{|}

---
 parsing/g_vernac.ml4              | 6 +++---
 test-suite/success/polymorphism.v | 2 ++
 2 files changed, 5 insertions(+), 3 deletions(-)

diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index d93c2563d7..59eb2b4d6c 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -238,9 +238,9 @@ GEXTEND Gram
   univ_decl :
     [ [  "@{" ; l = LIST0 identref; ext = [ "+" -> true | -> false ];
          cs = [ "|"; l' = LIST0 univ_constraint SEP ",";
-                ext = [ "+" -> true | -> false ] -> (l',ext)
-              | -> ([], true) ];
-         "}" ->
+                ext = [ "+" -> true | -> false ]; "}" -> (l',ext)
+              | ext = [ "}" -> true | "|}" -> false ] -> ([], ext) ]
+         ->
          { univdecl_instance = l;
            univdecl_extensible_instance = ext;
            univdecl_constraints = fst cs;
diff --git a/test-suite/success/polymorphism.v b/test-suite/success/polymorphism.v
index 0bd8bfe602..488443de1d 100644
--- a/test-suite/success/polymorphism.v
+++ b/test-suite/success/polymorphism.v
@@ -159,6 +159,8 @@ End structures.
 
 Module binders.
 
+  Definition mynat@{|} := nat.
+
   Definition foo@{i j | i < j, i < j} (A : Type@{i}) : Type@{j}.
     exact A.
   Defined.
-- 
cgit v1.2.3