From e715ae132c84960f766d64e7a17eea74924eadab Mon Sep 17 00:00:00 2001
From: Théo Zimmermann
Date: Sun, 23 Feb 2020 11:08:56 +0100
Subject: Fix #11654: syntax of inductive declaration.

Inductive foo := Bar |. was accepted but it shouldn't have.
---
 vernac/g_vernac.mlg | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg
index d597707d12..def4ed942a 100644
--- a/vernac/g_vernac.mlg
+++ b/vernac/g_vernac.mlg
@@ -402,7 +402,7 @@ GRAMMAR EXTEND Gram
   ;
   constructor_list_or_record_decl:
     [ [ "|"; l = LIST1 constructor SEP "|" -> { Constructors l }
-      | id = identref ; c = constructor_type; "|"; l = LIST0 constructor SEP "|" ->
+      | id = identref ; c = constructor_type; "|"; l = LIST1 constructor SEP "|" ->
           { Constructors ((c id)::l) }
       | id = identref ; c = constructor_type -> { Constructors [ c id ] }
       | cstr = identref; "{"; fs = record_fields; "}" ->
-- 
cgit v1.2.3