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

Reviewed-by: Zimmi48
Reviewed-by: ppedrot

17 files changed, 272 insertions, 90 deletions

diff --git a/doc/changelog/03-notations/11530-master+fix11331-custom-entries-precedence.rst b/doc/changelog/03-notations/11530-master+fix11331-custom-entries-precedence.rst
new file mode 100644
index 0000000000..b105928b22
--- /dev/null
+++ b/doc/changelog/03-notations/11530-master+fix11331-custom-entries-precedence.rst
@@ -0,0 +1,8 @@
+- **Fixed:**
+  Bugs in dealing with precedences of notations in custom entries
+  (`#11530 <https://github.com/coq/coq/pull/11530>`_,
+  by Hugo Herbelin, fixing in particular
+  `#9517 <https://github.com/coq/coq/pull/9517>`_,
+  `#9519 <https://github.com/coq/coq/pull/9519>`_,
+  `#9521 <https://github.com/coq/coq/pull/9521>`_,
+  `#11331 <https://github.com/coq/coq/pull/11331>`_).
diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst
index dbe714c388..a8d5ac610f 100644
--- a/doc/sphinx/user-extensions/syntax-extensions.rst
+++ b/doc/sphinx/user-extensions/syntax-extensions.rst
@@ -798,7 +798,13 @@ associated to the custom entry ``expr``. The level can be omitted, as in
 
    Notation "[ e ]" := e (e custom expr).
 
-in which case Coq tries to infer it.
+in which case Coq infer it. If the sub-expression is at a border of
+the notation (as e.g. ``x`` and ``y`` in ``x + y``), the level is
+determined by the associativity. If the sub-expression is not at the
+border of the notation (as e.g. ``e`` in ``"[ e ]``), the level is
+inferred to be the highest level used for the entry. In particular,
+this level depends on the highest level existing in the entry at the
+time of use of the notation.
 
 In the absence of an explicit entry for parsing or printing a
 sub-expression of a notation in a custom entry, the default is to
diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index c198c4eb9b..06232b8e1a 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -792,9 +792,11 @@ let rec flatten_application c = match DAst.get c with
 
 let extern_possible_prim_token (custom,scopes) r =
    let (sc,n) = uninterp_prim_token r in
-   match availability_of_entry_coercion custom InConstrEntrySomeLevel with
-   | None -> raise No_match
-   | Some coercion ->
+   let coercion =
+     if entry_has_prim_token n custom then [] else
+     match availability_of_entry_coercion custom InConstrEntrySomeLevel with
+     | None -> raise No_match
+     | Some coercion -> coercion in
    match availability_of_prim_token n sc scopes with
    | None -> raise No_match
    | Some key -> insert_coercion coercion (insert_delimiters (CAst.make ?loc:(loc_of_glob_constr r) @@ CPrim n) key)
diff --git a/interp/notation.ml b/interp/notation.ml
index 93969f3718..9d6cab550d 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -1349,6 +1349,34 @@ let entry_has_ident = function
   | InCustomEntryLevel (s,n) ->
      try String.Map.find s !entry_has_ident_map <= n with Not_found -> false
 
+let entry_has_numeral_map = ref String.Map.empty
+let entry_has_string_map = ref String.Map.empty
+
+let declare_custom_entry_has_numeral s n =
+  try
+    let p = String.Map.find s !entry_has_numeral_map in
+    user_err (str "Custom entry " ++ str s ++
+              str " has already a rule for numerals at level " ++ int p ++ str ".")
+  with Not_found ->
+    entry_has_numeral_map := String.Map.add s n !entry_has_numeral_map
+
+let declare_custom_entry_has_string s n =
+  try
+    let p = String.Map.find s !entry_has_string_map in
+    user_err (str "Custom entry " ++ str s ++
+              str " has already a rule for strings at level " ++ int p ++ str ".")
+  with Not_found ->
+    entry_has_string_map := String.Map.add s n !entry_has_string_map
+
+let entry_has_prim_token prim = function
+  | InConstrEntrySomeLevel -> true
+  | InCustomEntryLevel (s,n) ->
+     match prim with
+     | Numeral _ ->
+       (try String.Map.find s !entry_has_numeral_map <= n with Not_found -> false)
+     | String _ ->
+       (try String.Map.find s !entry_has_string_map <= n with Not_found -> false)
+
 let uninterp_prim_token c =
   match glob_prim_constr_key c with
   | None -> raise Notation_ops.No_match
diff --git a/interp/notation.mli b/interp/notation.mli
index ea5125f7ec..707be6cb87 100644
--- a/interp/notation.mli
+++ b/interp/notation.mli
@@ -305,9 +305,12 @@ val availability_of_entry_coercion : notation_entry_level -> notation_entry_leve
 
 val declare_custom_entry_has_global : string -> int -> unit
 val declare_custom_entry_has_ident : string -> int -> unit
+val declare_custom_entry_has_numeral : string -> int -> unit
+val declare_custom_entry_has_string : string -> int -> unit
 
 val entry_has_global : notation_entry_level -> bool
 val entry_has_ident : notation_entry_level -> bool
+val entry_has_prim_token : prim_token -> notation_entry_level -> bool
 
 (** Rem: printing rules for primitive token are canonical *)
 
diff --git a/parsing/extend.ml b/parsing/extend.ml
index dcdaa25c33..178f7354f2 100644
--- a/parsing/extend.ml
+++ b/parsing/extend.ml
@@ -21,6 +21,7 @@ type production_position =
 type production_level =
   | NextLevel
   | NumLevel of int
+  | DefaultLevel (** Interpreted differently at the border or inside a rule *)
 
 (** User-level types used to tell how to parse or interpret of the non-terminal *)
 
@@ -28,6 +29,7 @@ type 'a constr_entry_key_gen =
   | ETIdent
   | ETGlobal
   | ETBigint
+  | ETString
   | ETBinder of bool  (* open list of binders if true, closed list of binders otherwise *)
   | ETConstr of Constrexpr.notation_entry * Notation_term.constr_as_binder_kind option * 'a
   | ETPattern of bool * int option (* true = strict pattern, i.e. not a single variable *)
@@ -40,7 +42,7 @@ type constr_entry_key =
 (** Entries used in productions, vernac side (e.g. "x bigint" or "x ident") *)
 
 type simple_constr_prod_entry_key =
-    production_level option constr_entry_key_gen
+    production_level constr_entry_key_gen
 
 (** Entries used in productions (in right-hand-side of grammar rules), to parse non-terminals *)
 
@@ -52,6 +54,7 @@ type constr_prod_entry_key =
   | ETProdName            (* Parsed as a name (ident or _) *)
   | ETProdReference       (* Parsed as a global reference *)
   | ETProdBigint          (* Parsed as an (unbounded) integer *)
+  | ETProdString          (* Parsed as a string *)
   | ETProdConstr of Constrexpr.notation_entry * (production_level * production_position) (* Parsed as constr or pattern, or a subentry of those *)
   | ETProdPattern of int  (* Parsed as pattern as a binder (as subpart of a constr) *)
   | ETProdConstrList of Constrexpr.notation_entry * (production_level * production_position) * string Tok.p list (* Parsed as non-empty list of constr, or subentries of those *)
diff --git a/parsing/notgram_ops.ml b/parsing/notgram_ops.ml
index 009dafdb13..5c220abeda 100644
--- a/parsing/notgram_ops.ml
+++ b/parsing/notgram_ops.ml
@@ -48,17 +48,19 @@ let production_position_eq pp1 pp2 = match (pp1,pp2) with
 let production_level_eq l1 l2 = match (l1,l2) with
 | NextLevel, NextLevel -> true
 | NumLevel n1, NumLevel n2 -> Int.equal n1 n2
-| (NextLevel | NumLevel _), _ -> false
+| DefaultLevel, DefaultLevel -> true
+| (NextLevel | NumLevel _ | DefaultLevel), _ -> false
 
 let constr_entry_key_eq eq v1 v2 = match v1, v2 with
 | ETIdent, ETIdent -> true
 | ETGlobal, ETGlobal -> true
 | ETBigint, ETBigint -> true
+| ETString, ETString -> true
 | ETBinder b1, ETBinder b2 -> b1 == b2
 | ETConstr (s1,bko1,lev1), ETConstr (s2,bko2,lev2) ->
    notation_entry_eq s1 s2 && eq lev1 lev2 && Option.equal (=) bko1 bko2
 | ETPattern (b1,n1), ETPattern (b2,n2) -> b1 = b2 && Option.equal Int.equal n1 n2
-| (ETIdent | ETGlobal | ETBigint | ETBinder _ | ETConstr _ | ETPattern _), _ -> false
+| (ETIdent | ETGlobal | ETBigint | ETString | ETBinder _ | ETConstr _ | ETPattern _), _ -> false
 
 let level_eq_gen strict (s1, l1, t1, u1) (s2, l2, t2, u2) =
   let tolerability_eq (i1, r1) (i2, r2) = Int.equal i1 i2 && parenRelation_eq r1 r2 in
diff --git a/test-suite/bugs/closed/bug_9517.v b/test-suite/bugs/closed/bug_9517.v
new file mode 100644
index 0000000000..bb43edbe74
--- /dev/null
+++ b/test-suite/bugs/closed/bug_9517.v
@@ -0,0 +1,19 @@
+Declare Custom Entry expr.
+Declare Custom Entry stmt.
+Notation "x" := x (in custom stmt, x ident).
+Notation "x" := x (in custom expr, x ident).
+
+Notation "1" := 1 (in custom expr).
+
+Notation "! x = y !" := (pair x y) (in custom stmt at level 0, x custom expr, y custom expr).
+Notation "? x = y" := (pair x y) (in custom stmt at level 0, x custom expr, y custom expr).
+Notation "x = y" := (pair x y) (in custom stmt at level 0, x custom expr, y custom expr).
+
+Notation "stmt:( s )" := s (s custom stmt).
+Check stmt:(! _ = _ !).
+Check stmt:(? _ = _).
+Check stmt:(_ = _).
+Check stmt:(! 1 = 1 !).
+Check stmt:(? 1 = 1).
+Check stmt:(1 = 1).
+Check stmt:(_ = 1).
diff --git a/test-suite/bugs/closed/bug_9521.v b/test-suite/bugs/closed/bug_9521.v
new file mode 100644
index 0000000000..0464c62c09
--- /dev/null
+++ b/test-suite/bugs/closed/bug_9521.v
@@ -0,0 +1,23 @@
+(* Example from #9521 *)
+
+Module A.
+
+Declare Custom Entry expr.
+Notation "expr0:( s )" := s (s custom expr at level 0).
+Notation "#" := 0 (in custom expr at level 1).
+Check expr0:(#). (* Should not be an anomaly "unknown level 0" *)
+
+End A.
+
+(* Another example from a comment at #11561 *)
+
+Module B.
+
+Declare Custom Entry special.
+Declare Custom Entry expr.
+Notation "## x" := (S x) (in custom expr at level 10, x custom special at level 10).
+Notation "[ e ]" := e (e custom expr at level 10).
+Notation "1" := 1 (in custom special).
+Check [ ## 1 ].
+
+End B.
diff --git a/test-suite/bugs/closed/bug_9640.v b/test-suite/bugs/closed/bug_9640.v
new file mode 100644
index 0000000000..4dc0bead7b
--- /dev/null
+++ b/test-suite/bugs/closed/bug_9640.v
@@ -0,0 +1,23 @@
+(* Similar to #9521 (was an anomaly unknown level 150 *)
+
+Module A.
+
+Declare Custom Entry expr.
+Notation "p" := (p) (in custom expr at level 150, p constr, right associativity).
+Notation "** X" := (X) (at level 200, X custom expr at level 150).
+Lemma t : ** True.
+Abort.
+
+End A.
+
+(* Similar to #9517, #9519, #11331 *)
+
+Module B.
+
+Declare Custom Entry expr.
+Notation "p" := (p) (in custom expr at level 100, p constr (* at level 200 *)).
+Notation "** X" := (X) (at level 200, X custom expr at level 150).
+Lemma t : ** True.
+Abort.
+
+End B.
diff --git a/test-suite/output/Notations4.out b/test-suite/output/Notations4.out
index f65696e464..1c8f237bb8 100644
--- a/test-suite/output/Notations4.out
+++ b/test-suite/output/Notations4.out
@@ -14,6 +14,8 @@ Entry constr:myconstr is
      : nat
 [<< # 0 >>]
      : option nat
+[2 + 3]
+     : nat
 [1 {f 1}]
      : Expr
 fun (x : nat) (y z : Expr) => [1 + y z + {f x}]
@@ -71,3 +73,7 @@ The command has indeed failed with message:
 The format is not the same on the right- and left-hand sides of the special token "..".
 The command has indeed failed with message:
 The format is not the same on the right- and left-hand sides of the special token "..".
+Entry constr:expr is
+[ "201" RIGHTA
+  [ "{"; constr:operconstr LEVEL "200"; "}" ] ]
+
diff --git a/test-suite/output/Notations4.v b/test-suite/output/Notations4.v
index 4de6ce19b4..4ab800c9ba 100644
--- a/test-suite/output/Notations4.v
+++ b/test-suite/output/Notations4.v
@@ -22,6 +22,9 @@ Notation "<< x >>" := x (in custom myconstr at level 3, x custom anotherconstr a
 Notation "# x" := (Some x) (in custom anotherconstr at level 8, x constr at level 9).
 Check [ << # 0 >> ].
 
+Notation "n" := n%nat (in custom myconstr at level 0, n bigint).
+Check [ 2 + 3 ].
+
 End A.
 
 Module B.
@@ -184,3 +187,11 @@ Fail Notation " {@ T1 ; T2 ; .. ; Tn } " :=
   (format "'[v' {@  '[' T1 ']'  ;  '//' '['  T2  ']'   ;  '//' ..  ;   '//' '['  Tn  ']'  } ']'").
 
 End M.
+
+Module Bug11331.
+
+Declare Custom Entry expr.
+Notation "{ p }" := (p) (in custom expr at level 201, p constr).
+Print Custom Grammar expr.
+
+End Bug11331.
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