1 files changed, 17 insertions, 5 deletions

diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg
index a35a1998d3..2e777d9602 100644
--- a/vernac/g_vernac.mlg
+++ b/vernac/g_vernac.mlg
@@ -1087,6 +1087,11 @@ GRAMMAR EXTEND Gram
          r = red_expr ->
 	   { VernacDeclareReduction (s,r) }
 
+(* factorized here, though relevant for syntax extensions *)
+
+      | IDENT "Declare"; IDENT "Custom"; IDENT "Entry"; s = IDENT ->
+           { VernacDeclareCustomEntry s }
+
  ] ];
     END
 
@@ -1153,6 +1158,9 @@ GRAMMAR EXTEND Gram
   ;
   syntax_modifier:
     [ [ "at"; IDENT "level"; n = natural -> { SetLevel n }
+      | "in"; IDENT "custom"; x = IDENT -> { SetCustomEntry (x,None) }
+      | "in"; IDENT "custom"; x = IDENT; "at"; IDENT "level"; n = natural ->
+         { SetCustomEntry (x,Some n) }
       | IDENT "left"; IDENT "associativity" -> { SetAssoc LeftA }
       | IDENT "right"; IDENT "associativity" -> { SetAssoc RightA }
       | IDENT "no"; IDENT "associativity" -> { SetAssoc NonA }
@@ -1166,10 +1174,11 @@ GRAMMAR EXTEND Gram
           | { CAst.v = k }, Some s -> SetFormat(k,s)
           | s, None -> SetFormat ("text",s) end }
       | x = IDENT; ","; l = LIST1 [id = IDENT -> { id } ] SEP ","; "at";
-        lev = level -> { SetItemLevel (x::l,lev) }
-      | x = IDENT; "at"; lev = level -> { SetItemLevel ([x],lev) }
-      | x = IDENT; "at"; lev = level; b = constr_as_binder_kind -> { SetItemLevelAsBinder ([x],b,Some lev) }
-      | x = IDENT; b = constr_as_binder_kind -> { SetItemLevelAsBinder ([x],b,None) }
+        lev = level -> { SetItemLevel (x::l,None,Some lev) }
+      | x = IDENT; "at"; lev = level -> { SetItemLevel ([x],None,Some lev) }
+      | x = IDENT; "at"; lev = level; b = constr_as_binder_kind ->
+        { SetItemLevel ([x],Some b,Some lev) }
+      | x = IDENT; b = constr_as_binder_kind -> { SetItemLevel ([x],Some b,None) }
       | x = IDENT; typ = syntax_extension_type -> { SetEntryType (x,typ) }
     ] ]
   ;
@@ -1177,12 +1186,15 @@ GRAMMAR EXTEND Gram
     [ [ IDENT "ident" -> { ETName } | IDENT "global" -> { ETReference }
       | IDENT "bigint" -> { ETBigint }
       | IDENT "binder" -> { ETBinder true }
-      | IDENT "constr"; n = OPT at_level; b = constr_as_binder_kind -> { ETConstrAsBinder (b,n) }
+      | IDENT "constr" -> { ETConstr (InConstrEntry,None,None) }
+      | IDENT "constr"; n = OPT at_level; b = OPT constr_as_binder_kind -> { ETConstr (InConstrEntry,b,n) }
       | IDENT "pattern" -> { ETPattern (false,None) }
       | IDENT "pattern"; "at"; IDENT "level"; n = natural -> { ETPattern (false,Some n) }
       | IDENT "strict"; IDENT "pattern" -> { ETPattern (true,None) }
       | IDENT "strict"; IDENT "pattern"; "at"; IDENT "level"; n = natural -> { ETPattern (true,Some n) }
       | IDENT "closed"; IDENT "binder" -> { ETBinder false }
+      | IDENT "custom"; x = IDENT; n = OPT at_level; b = OPT constr_as_binder_kind ->
+           { ETConstr (InCustomEntry x,b,n) }
     ] ]
   ;
   at_level: