Merge PR #11530: Fixes custom entries precedence bugs (#11331 part)

Reviewed-by: Zimmi48
Reviewed-by: ppedrot

5 files changed, 131 insertions, 83 deletions

diff --git a/vernac/egramcoq.ml b/vernac/egramcoq.ml
index 07656f9715..5e98f5ddc0 100644
--- a/vernac/egramcoq.ml
+++ b/vernac/egramcoq.ml
@@ -200,41 +200,44 @@ let assoc_eq al ar =
   | LeftA, LeftA -> true
   | _, _ -> false
 
-(* [adjust_level assoc from prod] where [assoc] and [from] are the name
+(** [adjust_level assoc from prod] where [assoc] and [from] are the name
    and associativity of the level where to add the rule; the meaning of
    the result is
 
-     None = SELF
-     Some None = NEXT
-     Some (Some (n,cur)) = constr LEVEL n
-         s.t. if [cur] is set then [n] is the same as the [from] level *)
-let adjust_level assoc from = let open Gramlib.Gramext in function
+     DefaultLevel = entry name
+     NextLevel = NEXT
+     NumLevel n = constr LEVEL n *)
+let adjust_level custom assoc (custom',from) p = let open Gramlib.Gramext in match p with
+(* If a level in a different grammar, no other choice than denoting it by absolute level *)
+  | (NumLevel n,_) when not (Notation.notation_entry_eq custom custom') -> NumLevel n
+(* If a default level in a different grammar, the entry name is ok *)
+  | (DefaultLevel,InternalProd) ->
+    if Notation.notation_entry_eq custom InConstrEntry then NumLevel 200 else DefaultLevel
+  | (DefaultLevel,BorderProd _) when not (Notation.notation_entry_eq custom custom') ->
+    if Notation.notation_entry_eq custom InConstrEntry then NumLevel 200 else DefaultLevel
 (* Associativity is None means force the level *)
-  | (NumLevel n,BorderProd (_,None)) -> Some (Some (n,true))
+  | (NumLevel n,BorderProd (_,None)) -> NumLevel n
+  | (DefaultLevel,BorderProd (_,None)) -> assert false
 (* Compute production name on the right side *)
   (* If NonA or LeftA on the right-hand side, set to NEXT *)
-  | (NumLevel n,BorderProd (Right,Some (NonA|LeftA))) ->
-      Some None
+  | ((NumLevel _ | DefaultLevel),BorderProd (Right,Some (NonA|LeftA))) -> NextLevel
   (* If RightA on the right-hand side, set to the explicit (current) level *)
-  | (NumLevel n,BorderProd (Right,Some RightA)) ->
-      Some (Some (n,true))
+  | (NumLevel n,BorderProd (Right,Some RightA)) -> NumLevel n
+  | (DefaultLevel,BorderProd (Right,Some RightA)) -> NumLevel from
 (* Compute production name on the left side *)
   (* If NonA on the left-hand side, adopt the current assoc ?? *)
-  | (NumLevel n,BorderProd (Left,Some NonA)) -> None
+  | ((NumLevel _ | DefaultLevel),BorderProd (Left,Some NonA)) -> DefaultLevel
   (* If the expected assoc is the current one, set to SELF *)
-  | (NumLevel n,BorderProd (Left,Some a)) when assoc_eq a (camlp5_assoc assoc) ->
-      None
+  | ((NumLevel _ | DefaultLevel),BorderProd (Left,Some a)) when assoc_eq a (camlp5_assoc assoc) ->
+      DefaultLevel
   (* Otherwise, force the level, n or n-1, according to expected assoc *)
-  | (NumLevel n,BorderProd (Left,Some a)) ->
-    begin match a with
-    | LeftA -> Some (Some (n, true))
-    | _ -> Some None
-    end
+  | (NumLevel n,BorderProd (Left,Some LeftA)) -> NumLevel n
+  | ((NumLevel _ | DefaultLevel),BorderProd (Left,Some _)) -> NextLevel
   (* None means NEXT *)
-  | (NextLevel,_) -> Some None
+  | (NextLevel,_) -> assert (Notation.notation_entry_eq custom custom'); NextLevel
 (* Compute production name elsewhere *)
   | (NumLevel n,InternalProd) ->
-    if from = n + 1 then Some None else Some (Some (n, Int.equal n from))
+    if from = n + 1 then NextLevel else NumLevel n
 
 type _ target =
 | ForConstr : constr_expr target
@@ -246,6 +249,7 @@ type (_, _) entry =
 | TTName : ('self, lname) entry
 | TTReference : ('self, qualid) entry
 | TTBigint : ('self, string) entry
+| TTString : ('self, string) entry
 | TTConstr : notation_entry * prod_info * 'r target -> ('r, 'r) entry
 | TTConstrList : notation_entry * prod_info * string Tok.p list * 'r target -> ('r, 'r list) entry
 | TTPattern : int -> ('self, cases_pattern_expr) entry
@@ -311,13 +315,14 @@ let target_entry : type s. notation_entry -> s target -> s Entry.t = function
    | ForConstr -> entry_for_constr
    | ForPattern -> entry_for_patttern
 
-let is_self from e = match e with
+let is_self custom (custom',from) e = Notation.notation_entry_eq custom custom' && match e with
 | (NumLevel n, BorderProd (Right, _ (* Some(NonA|LeftA) *))) -> false
 | (NumLevel n, BorderProd (Left, _)) -> Int.equal from n
 | _ -> false
 
-let is_binder_level from e = match e with
-| (NumLevel 200, (BorderProd (Right, _) | InternalProd)) -> from = 200
+let is_binder_level custom (custom',from) e = match e with
+| (NumLevel 200, (BorderProd (Right, _) | InternalProd)) ->
+  custom = InConstrEntry && custom' = InConstrEntry && from = 200
 | _ -> false
 
 let make_sep_rules = function
@@ -338,15 +343,15 @@ type ('s, 'a) mayrec_symbol =
 | MayRecMay : ('s, mayrec, 'a) symbol -> ('s, 'a) mayrec_symbol
 
 let symbol_of_target : type s. _ -> _ -> _ -> _ -> s target -> (s, s) mayrec_symbol = fun custom p assoc from forpat ->
-  if custom = InConstrEntry && is_binder_level from p then MayRecNo (Aentryl (target_entry InConstrEntry forpat, "200"))
-  else if is_self from p then MayRecMay Aself
+  if is_binder_level custom from p then (* Prevent self *) MayRecNo (Aentryl (target_entry custom forpat, "200"))
+  else if is_self custom from p then MayRecMay Aself
   else
     let g = target_entry custom forpat in
-    let lev = adjust_level assoc from p in
+    let lev = adjust_level custom assoc from p in
     begin match lev with
-    | None -> MayRecNo (Aentry g)
-    | Some None -> MayRecMay Anext
-    | Some (Some (lev, cur)) -> MayRecNo (Aentryl (g, string_of_int lev))
+    | DefaultLevel -> MayRecNo (Aentry g)
+    | NextLevel -> MayRecMay Anext
+    | NumLevel lev -> MayRecNo (Aentryl (g, string_of_int lev))
     end
 
 let symbol_of_entry : type s r. _ -> _ -> (s, r) entry -> (s, r) mayrec_symbol = fun assoc from typ -> match typ with
@@ -365,12 +370,14 @@ let symbol_of_entry : type s r. _ -> _ -> (s, r) entry -> (s, r) mayrec_symbol =
 | TTName -> MayRecNo (Aentry Prim.name)
 | TTOpenBinderList -> MayRecNo (Aentry Constr.open_binders)
 | TTBigint -> MayRecNo (Aentry Prim.bigint)
+| TTString -> MayRecNo (Aentry Prim.string)
 | TTReference -> MayRecNo (Aentry Constr.global)
 
 let interp_entry forpat e = match e with
 | ETProdName -> TTAny TTName
 | ETProdReference -> TTAny TTReference
 | ETProdBigint -> TTAny TTBigint
+| ETProdString -> TTAny TTString
 | ETProdConstr (s,p) -> TTAny (TTConstr (s, p, forpat))
 | ETProdPattern p -> TTAny (TTPattern p)
 | ETProdConstrList (s, p, tkl) -> TTAny (TTConstrList (s, p, tkl, forpat))
@@ -410,6 +417,11 @@ match e with
   | ForConstr ->  push_constr subst (CAst.make @@ CPrim (Numeral (SPlus,NumTok.int v)))
   | ForPattern -> push_constr subst (CAst.make @@ CPatPrim (Numeral (SPlus,NumTok.int v)))
   end
+| TTString ->
+  begin match forpat with
+  | ForConstr ->  push_constr subst (CAst.make @@ CPrim (String v))
+  | ForPattern -> push_constr subst (CAst.make @@ CPatPrim (String v))
+  end
 | TTReference ->
   begin match forpat with
   | ForConstr  -> push_constr subst (CAst.make @@ CRef (v, None))
@@ -503,19 +515,24 @@ let prepare_empty_levels forpat (where,(pos,p4assoc,name,reinit)) =
   let empty = (pos, [(name, p4assoc, [])]) in
   ExtendRule (target_entry where forpat, reinit, empty)
 
-let rec pure_sublevels' custom assoc from forpat level = function
+let different_levels (custom,opt_level) (custom',string_level) =
+  match opt_level with
+  | None -> true
+  | Some level -> not (Notation.notation_entry_eq custom custom') || level <> int_of_string string_level
+
+let rec pure_sublevels' assoc from forpat level = function
 | [] -> []
 | GramConstrNonTerminal (e,_) :: rem ->
-   let rem = pure_sublevels' custom assoc from forpat level rem in
+   let rem = pure_sublevels' assoc from forpat level rem in
    let push where p rem =
-     match symbol_of_target custom p assoc from forpat with
-     | MayRecNo (Aentryl (_,i)) when level <> Some (int_of_string i) -> (where,int_of_string i) :: rem
+     match symbol_of_target where p assoc from forpat with
+     | MayRecNo (Aentryl (_,i)) when different_levels (fst from,level) (where,i) -> (where,int_of_string i) :: rem
      | _ -> rem in
    (match e with
    | ETProdPattern i -> push InConstrEntry (NumLevel i,InternalProd) rem
    | ETProdConstr (s,p) -> push s p rem
    | _ -> rem)
-| (GramConstrTerminal _ | GramConstrListMark _) :: rem -> pure_sublevels' custom assoc from forpat level rem
+| (GramConstrTerminal _ | GramConstrListMark _) :: rem -> pure_sublevels' assoc from forpat level rem
 
 let make_act : type r. r target -> _ -> r gen_eval = function
 | ForConstr -> fun notation loc env ->
@@ -530,8 +547,8 @@ let extend_constr state forpat ng =
   let assoc = ng.notgram_assoc in
   let (entry, level) = interp_constr_entry_key custom forpat n in
   let fold (accu, state) pt =
-    let AnyTyRule r = make_ty_rule assoc n forpat pt in
-    let pure_sublevels = pure_sublevels' custom assoc n forpat level pt in
+    let AnyTyRule r = make_ty_rule assoc (custom,n) forpat pt in
+    let pure_sublevels = pure_sublevels' assoc (custom,n) forpat level pt in
     let isforpat = target_to_bool forpat in
     let needed_levels, state = register_empty_levels state isforpat pure_sublevels in
     let (pos,p4assoc,name,reinit), state = find_position state custom isforpat assoc level in
diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg
index 74249301d7..97c9d23c68 100644
--- a/vernac/g_vernac.mlg
+++ b/vernac/g_vernac.mlg
@@ -1224,31 +1224,32 @@ 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,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) }
+        lev = level -> { SetItemLevel (x::l,None,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) }
     ] ]
   ;
   syntax_extension_type:
     [ [ IDENT "ident" -> { ETIdent } | IDENT "global" -> { ETGlobal }
       | IDENT "bigint" -> { ETBigint }
+      | IDENT "string" -> { ETString }
       | IDENT "binder" -> { ETBinder true }
-      | IDENT "constr" -> { ETConstr (InConstrEntry,None,None) }
-      | IDENT "constr"; n = OPT at_level; b = OPT constr_as_binder_kind -> { ETConstr (InConstrEntry,b,n) }
+      | IDENT "constr" -> { ETConstr (InConstrEntry,None,DefaultLevel) }
+      | IDENT "constr"; n = at_level_opt; 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 ->
+      | IDENT "custom"; x = IDENT; n = at_level_opt; b = OPT constr_as_binder_kind ->
            { ETConstr (InCustomEntry x,b,n) }
     ] ]
   ;
-  at_level:
-    [ [ "at"; n = level -> { n } ] ]
+  at_level_opt:
+    [ [ "at"; n = level -> { n }
+      | -> { DefaultLevel } ] ]
   ;
   constr_as_binder_kind:
     [ [ "as"; IDENT "ident" -> { Notation_term.AsIdent }
diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml
index 0c39aba70a..d39ee60c25 100644
--- a/vernac/metasyntax.ml
+++ b/vernac/metasyntax.ml
@@ -297,7 +297,11 @@ let precedence_of_position_and_level from_level = function
       n, let (lp,rp) = prec_assoc a in if b == Left then lp else rp
   | NumLevel n, InternalProd -> n, Prec n
   | NextLevel, _ -> from_level, L
+  | DefaultLevel, _ ->
+      (* Fake value, waiting for PR#5 at herbelin's fork *) 200,
+      Any
 
+(** Computing precedences of subentries for parsing *)
 let precedence_of_entry_type (from_custom,from_level) = function
   | ETConstr (custom,_,x) when notation_entry_eq custom from_custom ->
     precedence_of_position_and_level from_level x
@@ -309,6 +313,22 @@ let precedence_of_entry_type (from_custom,from_level) = function
   | ETPattern (_,n) -> let n = match n with None -> 0 | Some n -> n in n, Prec n
   | _ -> 0, E (* should not matter *)
 
+(** Computing precedences for future insertion of parentheses at
+    the time of printing using hard-wired constr levels *)
+let unparsing_precedence_of_entry_type from_level = function
+  | ETConstr (InConstrEntry,_,x) ->
+    (* Possible insertion of parentheses at printing time to deal
+       with precedence in a constr entry is managed using [prec_less]
+       in [ppconstr.ml] *)
+    snd (precedence_of_position_and_level from_level x)
+  | ETConstr (custom,_,_) ->
+    (* Precedence of printing for a custom entry is managed using
+       explicit insertion of entry coercions at the time of building
+       a [constr_expr] *)
+    Any
+  | ETPattern (_,n) -> (* in constr *) Prec (match n with Some n -> n | None -> 0)
+  | _ -> Any (* should not matter *)
+
 (* Some breaking examples *)
 (* "x = y" : "x /1 = y" (breaks before any symbol) *)
 (* "x =S y" : "x /1 =S /1 y" (protect from confusion; each side for symmetry)*)
@@ -374,9 +394,9 @@ let check_open_binder isopen sl m =
 
 let unparsing_metavar i from typs =
   let x = List.nth typs (i-1) in
-  let prec = snd (precedence_of_entry_type from x) in
+  let prec = unparsing_precedence_of_entry_type from x in
   match x with
-  | ETConstr _ | ETGlobal | ETBigint ->
+  | ETConstr _ | ETGlobal | ETBigint | ETString ->
      UnpMetaVar (i,prec)
   | ETPattern _ ->
      UnpBinderMetaVar (i,prec)
@@ -389,12 +409,12 @@ let unparsing_metavar i from typs =
 
 let index_id id l = List.index Id.equal id l
 
-let make_hunks etyps symbols from =
+let make_hunks etyps symbols from_level =
   let vars,typs = List.split etyps in
   let rec make b = function
     | NonTerminal m :: prods ->
         let i = index_id m vars in
-        let u = unparsing_metavar i from typs in
+        let u = unparsing_metavar i from_level typs in
         if is_next_non_terminal b prods then
           (None, u) :: add_break_if_none 1 b (make b prods)
         else
@@ -428,7 +448,7 @@ let make_hunks etyps symbols from =
     | SProdList (m,sl) :: prods ->
         let i = index_id m vars in
         let typ = List.nth typs (i-1) in
-        let _,prec = precedence_of_entry_type from typ in
+        let prec = unparsing_precedence_of_entry_type from_level typ in
         let sl' =
           (* If no separator: add a break *)
           if List.is_empty sl then add_break 1 []
@@ -555,7 +575,7 @@ let read_recursive_format sl fmt =
      the names in the notation *)
   slfmt, res
 
-let hunks_of_format (from,(vars,typs)) symfmt =
+let hunks_of_format (from_level,(vars,typs)) symfmt =
   let rec aux = function
   | symbs, (_,(UnpTerminal s' as u)) :: fmt
       when String.equal s' (String.make (String.length s') ' ') ->
@@ -565,13 +585,13 @@ let hunks_of_format (from,(vars,typs)) symfmt =
       let symbs, l = aux (symbs,fmt) in symbs, UnpTerminal s :: l
   | NonTerminal s :: symbs, (_,UnpTerminal s') :: fmt when Id.equal s (Id.of_string s') ->
       let i = index_id s vars in
-      let symbs, l = aux (symbs,fmt) in symbs, unparsing_metavar i from typs :: l
+      let symbs, l = aux (symbs,fmt) in symbs, unparsing_metavar i from_level typs :: l
   | symbs, (_,(UnpCut _ as u)) :: fmt ->
       let symbs, l = aux (symbs,fmt) in symbs, u :: l
   | SProdList (m,sl) :: symbs, fmt when has_ldots fmt ->
       let i = index_id m vars in
       let typ = List.nth typs (i-1) in
-      let _,prec = precedence_of_entry_type from typ in
+      let prec = unparsing_precedence_of_entry_type from_level typ in
       let loc_slfmt,rfmt = read_recursive_format sl fmt in
       let sl, slfmt = aux (sl,loc_slfmt) in
       if not (List.is_empty sl) then error_format ?loc:(find_prod_list_loc loc_slfmt fmt) ();
@@ -666,6 +686,7 @@ let prod_entry_type = function
   | ETIdent -> ETProdName
   | ETGlobal -> ETProdReference
   | ETBigint -> ETProdBigint
+  | ETString -> ETProdString
   | ETBinder _ -> assert false (* See check_binder_type *)
   | ETConstr (s,_,p) -> ETProdConstr (s,p)
   | ETPattern (_,n) -> ETProdPattern (match n with None -> 0 | Some n -> n)
@@ -955,18 +976,23 @@ let is_only_printing mods =
 
 (* Compute precedences from modifiers (or find default ones) *)
 
-let set_entry_type from etyps (x,typ) =
+let set_entry_type from n etyps (x,typ) =
+  let make_lev n s = match typ with
+    | BorderProd _ -> NumLevel n
+    | InternalProd -> DefaultLevel in
   let typ = try
     match List.assoc x etyps, typ with
-      | ETConstr (s,bko,Some n), (_,BorderProd (left,_)) ->
+      | ETConstr (s,bko,DefaultLevel), _ ->
+         if notation_entry_eq from s then ETConstr (s,bko,(make_lev n s,typ))
+         else ETConstr (s,bko,(DefaultLevel,typ))
+      | ETConstr (s,bko,n), BorderProd (left,_) ->
           ETConstr (s,bko,(n,BorderProd (left,None)))
-      | ETConstr (s,bko,Some n), (_,InternalProd) ->
-         ETConstr (s,bko,(n,InternalProd))
+      | ETConstr (s,bko,n), InternalProd ->
+          ETConstr (s,bko,(n,InternalProd))
       | ETPattern (b,n), _ -> ETPattern (b,n)
-      | (ETIdent | ETBigint | ETGlobal | ETBinder _ as x), _ -> x
-      | ETConstr (s,bko,None), _ -> ETConstr (s,bko,typ)
+      | (ETIdent | ETBigint | ETString | ETGlobal | ETBinder _ as x), _ -> x
     with Not_found ->
-      ETConstr (from,None,typ)
+      ETConstr (from,None,(make_lev n from,typ))
   in (x,typ)
 
 let join_auxiliary_recursive_types recvars etyps =
@@ -986,7 +1012,7 @@ let join_auxiliary_recursive_types recvars etyps =
 
 let internalization_type_of_entry_type = function
   | ETBinder _ -> NtnInternTypeOnlyBinder
-  | ETConstr _ | ETBigint | ETGlobal
+  | ETConstr _ | ETBigint | ETString | ETGlobal
   | ETIdent | ETPattern _ -> NtnInternTypeAny
 
 let set_internalization_type typs =
@@ -1008,7 +1034,7 @@ let make_interpretation_type isrec isonlybinding = function
   (* Others *)
   | ETIdent -> NtnTypeBinder NtnParsedAsIdent
   | ETPattern (ppstrict,_) -> NtnTypeBinder (NtnParsedAsPattern ppstrict) (* Parsed as ident/pattern, primarily interpreted as binder; maybe strict at printing *)
-  | ETBigint | ETGlobal -> NtnTypeConstr
+  | ETBigint | ETString | ETGlobal -> NtnTypeConstr
   | ETBinder _ ->
      if isrec then NtnTypeBinderList
      else anomaly Pp.(str "Type binder is only for use in recursive notations for binders.")
@@ -1072,6 +1098,8 @@ type entry_coercion_kind =
   | IsEntryCoercion of notation_entry_level
   | IsEntryGlobal of string * int
   | IsEntryIdent of string * int
+  | IsEntryNumeral of string * int
+  | IsEntryString of string * int
 
 let is_coercion = function
   | Some (custom,n,_,[e]) ->
@@ -1083,6 +1111,8 @@ let is_coercion = function
          else Some (IsEntryCoercion subentry)
      | ETGlobal, InCustomEntry s -> Some (IsEntryGlobal (s,n))
      | ETIdent, InCustomEntry s -> Some (IsEntryIdent (s,n))
+     | ETBigint, InCustomEntry s -> Some (IsEntryNumeral (s,n))
+     | ETString, InCustomEntry s -> Some (IsEntryString (s,n))
      | _ -> None)
   | Some _ -> assert false
   | None -> None
@@ -1123,8 +1153,8 @@ let find_precedence custom lev etyps symbols onlyprint =
         else
           user_err Pp.(str "The level of the leftmost non-terminal cannot be changed.") in
       (try match List.assoc x etyps, custom with
-        | ETConstr (s,_,Some _), s' when s = s' -> test ()
-        | (ETIdent | ETBigint | ETGlobal), _ ->
+        | ETConstr (s,_,(NumLevel _ | NextLevel)), s' when s = s' -> test ()
+        | (ETIdent | ETBigint | ETString | ETGlobal), _ ->
             begin match lev with
             | None ->
               ([Feedback.msg_info ?loc:None ,strbrk "Setting notation at level 0."],0)
@@ -1216,14 +1246,13 @@ module SynData = struct
 end
 
 let find_subentry_types from n assoc etyps symbols =
-  let innerlevel = NumLevel 200 in
   let typs =
     find_symbols
-      (NumLevel n,BorderProd(Left,assoc))
-      (innerlevel,InternalProd)
-      (NumLevel n,BorderProd(Right,assoc))
+      (BorderProd(Left,assoc))
+      (InternalProd)
+      (BorderProd(Right,assoc))
       symbols in
-  let sy_typs = List.map (set_entry_type from etyps) typs in
+  let sy_typs = List.map (set_entry_type from n etyps) typs in
   let prec = List.map (assoc_of_type from n) sy_typs in
   sy_typs, prec
 
@@ -1351,6 +1380,8 @@ let open_notation i (_, nobj) =
     | Some (IsEntryCoercion entry) -> Notation.declare_entry_coercion ntn entry
     | Some (IsEntryGlobal (entry,n)) -> Notation.declare_custom_entry_has_global entry n
     | Some (IsEntryIdent (entry,n)) -> Notation.declare_custom_entry_has_ident entry n
+    | Some (IsEntryNumeral (entry,n)) -> Notation.declare_custom_entry_has_numeral entry n
+    | Some (IsEntryString (entry,n)) -> Notation.declare_custom_entry_has_string entry n
     | None -> ())
   end
 
@@ -1445,7 +1476,7 @@ let make_syntax_rules (sd : SynData.syn_data) = let open SynData in
   let ntn_for_grammar, prec_for_grammar, need_squash = sd.not_data in
   let custom,level,_,_ = sd.level in
   let pa_rule = make_pa_rule prec_for_grammar sd.pa_syntax_data ntn_for_grammar need_squash in
-  let pp_rule = make_pp_rule (custom,level) sd.pp_syntax_data sd.format in {
+  let pp_rule = make_pp_rule level sd.pp_syntax_data sd.format in {
     synext_level    = sd.level;
     synext_notation = fst sd.info;
     synext_notgram  = { notgram_onlyprinting = sd.only_printing; notgram_rules = pa_rule };
diff --git a/vernac/ppvernac.ml b/vernac/ppvernac.ml
index 6240120cb0..0cf407619b 100644
--- a/vernac/ppvernac.ml
+++ b/vernac/ppvernac.ml
@@ -107,8 +107,11 @@ open Pputils
     | InCustomEntry s -> keyword "custom" ++ spc () ++ str s
 
   let pr_at_level = function
-    | NumLevel n -> keyword "at" ++ spc () ++ keyword "level" ++ spc () ++ int n
-    | NextLevel -> keyword "at" ++ spc () ++ keyword "next" ++ spc () ++ keyword "level"
+    | NumLevel n -> spc () ++ keyword "at" ++ spc () ++ keyword "level" ++ spc () ++ int n
+    | NextLevel -> spc () ++ keyword "at" ++ spc () ++ keyword "next" ++ spc () ++ keyword "level"
+    | DefaultLevel -> mt ()
+
+  let level_of_pattern_level = function None -> DefaultLevel | Some n -> NumLevel n
 
   let pr_constr_as_binder_kind = let open Notation_term in function
     | AsIdent -> spc () ++ keyword "as ident"
@@ -120,19 +123,15 @@ open Pputils
   let pr_set_entry_type pr = function
     | ETIdent -> str"ident"
     | ETGlobal -> str"global"
-    | ETPattern (b,None) -> pr_strict b ++ str"pattern"
-    | ETPattern (b,Some n) -> pr_strict b ++ str"pattern" ++ spc () ++ pr_at_level (NumLevel n)
+    | ETPattern (b,n) -> pr_strict b ++ str"pattern" ++ pr_at_level (level_of_pattern_level n)
     | ETConstr (s,bko,lev) -> pr_notation_entry s ++ pr lev ++ pr_opt pr_constr_as_binder_kind bko
     | ETBigint -> str "bigint"
+    | ETString -> str "string"
     | ETBinder true -> str "binder"
     | ETBinder false -> str "closed binder"
 
-  let pr_at_level_opt = function
-    | None -> mt ()
-    | Some n -> spc () ++ pr_at_level n
-
   let pr_set_simple_entry_type =
-    pr_set_entry_type pr_at_level_opt
+    pr_set_entry_type pr_at_level
 
   let pr_comment pr_c = function
     | CommentConstr c -> pr_c c
@@ -402,7 +401,7 @@ let string_of_theorem_kind = let open Decls in function
 
   let pr_syntax_modifier = let open Gramlib.Gramext in function
     | SetItemLevel (l,bko,n) ->
-      prlist_with_sep sep_v2 str l ++ spc () ++ pr_at_level_opt n ++
+      prlist_with_sep sep_v2 str l ++ spc () ++ pr_at_level n ++
       pr_opt pr_constr_as_binder_kind bko
     | SetLevel n -> pr_at_level (NumLevel n)
     | SetCustomEntry (s,n) -> keyword "in" ++ spc() ++ keyword "custom" ++ spc() ++ str s ++ (match n with None -> mt () | Some n -> pr_at_level (NumLevel n))
diff --git a/vernac/vernacexpr.ml b/vernac/vernacexpr.ml
index 8ead56dfdf..3610240634 100644
--- a/vernac/vernacexpr.ml
+++ b/vernac/vernacexpr.ml
@@ -177,7 +177,7 @@ type proof_expr =
   ident_decl * (local_binder_expr list * constr_expr)
 
 type syntax_modifier =
-  | SetItemLevel of string list * Notation_term.constr_as_binder_kind option * Extend.production_level option
+  | SetItemLevel of string list * Notation_term.constr_as_binder_kind option * Extend.production_level
   | SetLevel of int
   | SetCustomEntry of string * int option
   | SetAssoc of Gramlib.Gramext.g_assoc