From cb3744bbf5165851877e17c12e92b40027526a04 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Mon, 10 Feb 2020 17:37:10 +0100
Subject: Mini-factorization in vernac grammar.

Unfortunately, we cannot factorize further

| x = IDENT; "at"; lev = level; b = OPT constr_as_binder_kind
| x = IDENT; b = constr_as_binder_kind

without losing the rule

| x = IDENT; typ = syntax_extension_type
---
 vernac/g_vernac.mlg | 5 ++---
 1 file changed, 2 insertions(+), 3 deletions(-)

diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg
index ac2341ac8d..28b9fa7449 100644
--- a/vernac/g_vernac.mlg
+++ b/vernac/g_vernac.mlg
@@ -1225,9 +1225,8 @@ GRAMMAR EXTEND Gram
           | s, None -> SetFormat ("text",s) end }
       | x = IDENT; ","; l = LIST1 [id = IDENT -> { id } ] SEP ","; "at";
         lev = level -> { SetItemLevel (x::l,None,lev) }
-      | x = IDENT; "at"; lev = level -> { SetItemLevel ([x],None,lev) }
-      | x = IDENT; "at"; lev = level; b = constr_as_binder_kind ->
-        { SetItemLevel ([x],Some b,lev) }
+      | x = IDENT; "at"; lev = level; b = OPT constr_as_binder_kind ->
+        { SetItemLevel ([x],b,lev) }
       | x = IDENT; b = constr_as_binder_kind -> { SetItemLevel ([x],Some b,DefaultLevel) }
       | x = IDENT; typ = syntax_extension_type -> { SetEntryType (x,typ) }
     ] ]
-- 
cgit v1.2.3