From 44ec3c8fd02f27d1dc7123bfbe5f5018937d6b86 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Wed, 25 Dec 2019 13:57:00 +0100
Subject: Fixes #11331 (unexpected level collisions between custom entries and
 constr).

There was a collision at the time of interpreting subentries (in
metasyntax.ml) but also at the time of "optimizing" the entries (in
egramcoq.ml).

Also fixes #9517, fixes #9519, fixes #9640 (part 3).
---
 test-suite/bugs/closed/bug_9517.v | 19 +++++++++++++++++++
 test-suite/output/Notations4.out  |  4 ++++
 test-suite/output/Notations4.v    |  8 ++++++++
 vernac/egramcoq.ml                | 31 +++++++++++++++++--------------
 vernac/metasyntax.ml              | 31 ++++++++++++++++++++-----------
 5 files changed, 68 insertions(+), 25 deletions(-)
 create mode 100644 test-suite/bugs/closed/bug_9517.v

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/output/Notations4.out b/test-suite/output/Notations4.out
index f65696e464..807914a671 100644
--- a/test-suite/output/Notations4.out
+++ b/test-suite/output/Notations4.out
@@ -71,3 +71,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..2906698386 100644
--- a/test-suite/output/Notations4.v
+++ b/test-suite/output/Notations4.v
@@ -184,3 +184,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..65a51f648e 100644
--- a/vernac/egramcoq.ml
+++ b/vernac/egramcoq.ml
@@ -208,7 +208,9 @@ let assoc_eq al ar =
      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
+let adjust_level custom assoc (custom',from) p = let open Gramlib.Gramext in match p with
+(* If in a different grammar, no other choice than denoting it by absolute level *)
+  | (NumLevel n,_) when not (Notation.notation_entry_eq custom custom') -> Some (Some (n,true))
 (* Associativity is None means force the level *)
   | (NumLevel n,BorderProd (_,None)) -> Some (Some (n,true))
 (* Compute production name on the right side *)
@@ -231,7 +233,7 @@ let adjust_level assoc from = let open Gramlib.Gramext in function
     | _ -> Some None
     end
   (* None means NEXT *)
-  | (NextLevel,_) -> Some None
+  | (NextLevel,_) -> assert (Notation.notation_entry_eq custom custom'); Some None
 (* Compute production name elsewhere *)
   | (NumLevel n,InternalProd) ->
     if from = n + 1 then Some None else Some (Some (n, Int.equal n from))
@@ -311,13 +313,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,11 +341,11 @@ 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
@@ -503,19 +506,19 @@ 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 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
+     match symbol_of_target where p assoc from forpat with
      | MayRecNo (Aentryl (_,i)) when level <> Some (int_of_string 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 +533,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/metasyntax.ml b/vernac/metasyntax.ml
index 0c39aba70a..ecfebec6b8 100644
--- a/vernac/metasyntax.ml
+++ b/vernac/metasyntax.ml
@@ -955,18 +955,28 @@ 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 ->
+      if s = InConstrEntry then NumLevel 200 else
+      user_err (strbrk "level of inner subentry " ++ quote (pr_notation_entry s) ++
+                str " cannot be inferred. It must be given explicitly.") in
   let typ = try
     match List.assoc x etyps, typ with
-      | ETConstr (s,bko,Some n), (_,BorderProd (left,_)) ->
+      | ETConstr (s,bko,Some n), BorderProd (left,_) ->
           ETConstr (s,bko,(n,BorderProd (left,None)))
-      | ETConstr (s,bko,Some n), (_,InternalProd) ->
-         ETConstr (s,bko,(n,InternalProd))
+      | ETConstr (s,bko,Some 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)
+      | ETConstr (s,bko,None), _ ->
+         if notation_entry_eq from s then ETConstr (s,bko,(make_lev n s,typ))
+         else if s = InConstrEntry then ETConstr (s,bko,(make_lev 200 s,typ)) else
+         user_err (strbrk "level of subentry " ++ quote (pr_notation_entry s) ++
+                   str " cannot be inferred. It must be given explicitly.")
     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 =
@@ -1216,14 +1226,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
 
-- 
cgit v1.2.3


From af8ddf0038e0caac1763da7ef510e4d5fdd4b8e7 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Wed, 25 Dec 2019 14:00:16 +0100
Subject: Fixing a precedence printing bug with custom entries.

Insertion of coercion to manage precedence of custom entries are
treated in constrextern.ml, while ppconstr.ml is only about the
management of precedences for constr.
---
 vernac/metasyntax.ml | 33 +++++++++++++++++++++++++--------
 1 file changed, 25 insertions(+), 8 deletions(-)

diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml
index ecfebec6b8..c8c2376155 100644
--- a/vernac/metasyntax.ml
+++ b/vernac/metasyntax.ml
@@ -298,6 +298,7 @@ let precedence_of_position_and_level from_level = function
   | NumLevel n, InternalProd -> n, Prec n
   | NextLevel, _ -> from_level, L
 
+(** 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 +310,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,7 +391,7 @@ 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 ->
      UnpMetaVar (i,prec)
@@ -389,12 +406,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 +445,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 +572,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 +582,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) ();
@@ -1454,7 +1471,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 };
-- 
cgit v1.2.3


From 7985e4f9422216566d7d4675f8c562da9b989d0f Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Mon, 10 Feb 2020 14:15:46 +0100
Subject: Dead code in Egramcoq.adjust_level.

---
 vernac/egramcoq.ml | 15 +++++++--------
 1 file changed, 7 insertions(+), 8 deletions(-)

diff --git a/vernac/egramcoq.ml b/vernac/egramcoq.ml
index 65a51f648e..2b6b18e058 100644
--- a/vernac/egramcoq.ml
+++ b/vernac/egramcoq.ml
@@ -206,20 +206,19 @@ let assoc_eq al ar =
 
      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 *)
+     Some (Some (n,cur)) = constr LEVEL n *)
 let adjust_level custom assoc (custom',from) p = let open Gramlib.Gramext in match p with
 (* If in a different grammar, no other choice than denoting it by absolute level *)
-  | (NumLevel n,_) when not (Notation.notation_entry_eq custom custom') -> Some (Some (n,true))
+  | (NumLevel n,_) when not (Notation.notation_entry_eq custom custom') -> Some (Some n)
 (* Associativity is None means force the level *)
-  | (NumLevel n,BorderProd (_,None)) -> Some (Some (n,true))
+  | (NumLevel n,BorderProd (_,None)) -> Some (Some n)
 (* 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
   (* If RightA on the right-hand side, set to the explicit (current) level *)
   | (NumLevel n,BorderProd (Right,Some RightA)) ->
-      Some (Some (n,true))
+      Some (Some n)
 (* 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
@@ -229,14 +228,14 @@ let adjust_level custom assoc (custom',from) p = let open Gramlib.Gramext in mat
   (* 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))
+    | LeftA -> Some (Some n)
     | _ -> Some None
     end
   (* None means NEXT *)
   | (NextLevel,_) -> assert (Notation.notation_entry_eq custom custom'); Some None
 (* 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 Some None else Some (Some n)
 
 type _ target =
 | ForConstr : constr_expr target
@@ -349,7 +348,7 @@ let symbol_of_target : type s. _ -> _ -> _ -> _ -> s target -> (s, s) mayrec_sym
     begin match lev with
     | None -> MayRecNo (Aentry g)
     | Some None -> MayRecMay Anext
-    | Some (Some (lev, cur)) -> MayRecNo (Aentryl (g, string_of_int lev))
+    | Some (Some 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
-- 
cgit v1.2.3


From 45ced1c1af3dbe7f81c8b928aeb76ebadfe709ea Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Mon, 10 Feb 2020 17:27:21 +0100
Subject: Reorganize type "production_level" along a more intuitive structure.

NextLevel    = at next level
NumLevel n   = at level n
DefaultLevel = <no mention of level>
---
 parsing/extend.ml      |  3 ++-
 parsing/notgram_ops.ml |  3 ++-
 vernac/egramcoq.ml     | 22 +++++++++++++---------
 vernac/g_vernac.mlg    | 19 ++++++++++---------
 vernac/metasyntax.ml   | 19 +++++++++++--------
 vernac/ppvernac.ml     | 18 ++++++++----------
 vernac/vernacexpr.ml   |  2 +-
 7 files changed, 47 insertions(+), 39 deletions(-)

diff --git a/parsing/extend.ml b/parsing/extend.ml
index dcdaa25c33..848861238a 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 *)
 
@@ -40,7 +41,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 *)
 
diff --git a/parsing/notgram_ops.ml b/parsing/notgram_ops.ml
index 009dafdb13..a5ade43295 100644
--- a/parsing/notgram_ops.ml
+++ b/parsing/notgram_ops.ml
@@ -48,7 +48,8 @@ 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
diff --git a/vernac/egramcoq.ml b/vernac/egramcoq.ml
index 2b6b18e058..1c1b59e397 100644
--- a/vernac/egramcoq.ml
+++ b/vernac/egramcoq.ml
@@ -208,29 +208,33 @@ let assoc_eq al ar =
      Some None = NEXT
      Some (Some (n,cur)) = constr LEVEL n *)
 let adjust_level custom assoc (custom',from) p = let open Gramlib.Gramext in match p with
-(* If in a different grammar, no other choice than denoting it by absolute level *)
+(* 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') -> Some (Some n)
+(* If a default level in a different grammar, the entry name is ok *)
+  | (DefaultLevel,InternalProd) ->
+    if Notation.notation_entry_eq custom InConstrEntry then Some (Some 200) else None
+  | (DefaultLevel,BorderProd _) when not (Notation.notation_entry_eq custom custom') -> None
 (* Associativity is None means force the level *)
   | (NumLevel n,BorderProd (_,None)) -> Some (Some 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))) ->
+  | ((NumLevel _ | DefaultLevel),BorderProd (Right,Some (NonA|LeftA))) ->
       Some None
   (* If RightA on the right-hand side, set to the explicit (current) level *)
   | (NumLevel n,BorderProd (Right,Some RightA)) ->
       Some (Some n)
+  | (DefaultLevel,BorderProd (Right,Some RightA)) ->
+      Some (Some 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)) -> None
   (* If the expected assoc is the current one, set to SELF *)
-  | (NumLevel n,BorderProd (Left,Some a)) when assoc_eq a (camlp5_assoc assoc) ->
+  | ((NumLevel _ | DefaultLevel),BorderProd (Left,Some a)) when assoc_eq a (camlp5_assoc assoc) ->
       None
   (* 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)
-    | _ -> Some None
-    end
+  | (NumLevel n,BorderProd (Left,Some LeftA)) -> Some (Some n)
+  | ((NumLevel _ | DefaultLevel),BorderProd (Left,Some _)) -> Some None
   (* None means NEXT *)
   | (NextLevel,_) -> assert (Notation.notation_entry_eq custom custom'); Some None
 (* Compute production name elsewhere *)
diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg
index 74249301d7..ac2341ac8d 100644
--- a/vernac/g_vernac.mlg
+++ b/vernac/g_vernac.mlg
@@ -1224,11 +1224,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,None,Some lev) }
-      | x = IDENT; "at"; lev = level -> { SetItemLevel ([x],None,Some lev) }
+        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,Some lev) }
-      | x = IDENT; b = constr_as_binder_kind -> { SetItemLevel ([x],Some b,None) }
+        { SetItemLevel ([x],Some b,lev) }
+      | x = IDENT; b = constr_as_binder_kind -> { SetItemLevel ([x],Some b,DefaultLevel) }
       | x = IDENT; typ = syntax_extension_type -> { SetEntryType (x,typ) }
     ] ]
   ;
@@ -1236,19 +1236,20 @@ GRAMMAR EXTEND Gram
     [ [ IDENT "ident" -> { ETIdent } | IDENT "global" -> { ETGlobal }
       | IDENT "bigint" -> { ETBigint }
       | 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 c8c2376155..1e46d35ed7 100644
--- a/vernac/metasyntax.ml
+++ b/vernac/metasyntax.ml
@@ -297,6 +297,9 @@ 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
@@ -981,17 +984,17 @@ let set_entry_type from n etyps (x,typ) =
                 str " cannot be inferred. It must be given explicitly.") in
   let typ = try
     match List.assoc x etyps, typ with
-      | ETConstr (s,bko,Some n), BorderProd (left,_) ->
-          ETConstr (s,bko,(n,BorderProd (left,None)))
-      | ETConstr (s,bko,Some 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,DefaultLevel), _ ->
          if notation_entry_eq from s then ETConstr (s,bko,(make_lev n s,typ))
          else if s = InConstrEntry then ETConstr (s,bko,(make_lev 200 s,typ)) else
          user_err (strbrk "level of subentry " ++ quote (pr_notation_entry s) ++
                    str " cannot be inferred. It must be given explicitly.")
+      | ETConstr (s,bko,n), BorderProd (left,_) ->
+          ETConstr (s,bko,(n,BorderProd (left,None)))
+      | ETConstr (s,bko,n), InternalProd ->
+          ETConstr (s,bko,(n,InternalProd))
+      | ETPattern (b,n), _ -> ETPattern (b,n)
+      | (ETIdent | ETBigint | ETGlobal | ETBinder _ as x), _ -> x
     with Not_found ->
       ETConstr (from,None,(make_lev n from,typ))
   in (x,typ)
@@ -1150,7 +1153,7 @@ 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 ()
+        | ETConstr (s,_,(NumLevel _ | NextLevel)), s' when s = s' -> test ()
         | (ETIdent | ETBigint | ETGlobal), _ ->
             begin match lev with
             | None ->
diff --git a/vernac/ppvernac.ml b/vernac/ppvernac.ml
index 6240120cb0..f4918caeff 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,14 @@ 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"
     | 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 +400,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
-- 
cgit v1.2.3


From 376e92f87a73afb9d848cea9895d75c932b2b25a Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Mon, 10 Feb 2020 22:36:14 +0100
Subject: Reusing type production_level for the result of adjust_level.

---
 vernac/egramcoq.ml | 43 ++++++++++++++++++++-----------------------
 1 file changed, 20 insertions(+), 23 deletions(-)

diff --git a/vernac/egramcoq.ml b/vernac/egramcoq.ml
index 1c1b59e397..bf49fb4df5 100644
--- a/vernac/egramcoq.ml
+++ b/vernac/egramcoq.ml
@@ -200,46 +200,43 @@ 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 *)
+     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') -> Some (Some n)
+  | (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 Some (Some 200) else None
-  | (DefaultLevel,BorderProd _) when not (Notation.notation_entry_eq custom custom') -> None
+    if Notation.notation_entry_eq custom InConstrEntry then NumLevel 200 else DefaultLevel
+  | (DefaultLevel,BorderProd _) when not (Notation.notation_entry_eq custom custom') -> DefaultLevel
 (* Associativity is None means force the level *)
-  | (NumLevel n,BorderProd (_,None)) -> Some (Some n)
+  | (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 _ | DefaultLevel),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)
-  | (DefaultLevel,BorderProd (Right,Some RightA)) ->
-      Some (Some from)
+  | (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 _ | DefaultLevel),BorderProd (Left,Some NonA)) -> None
+  | ((NumLevel _ | DefaultLevel),BorderProd (Left,Some NonA)) -> DefaultLevel
   (* If the expected assoc is the current one, set to SELF *)
   | ((NumLevel _ | DefaultLevel),BorderProd (Left,Some a)) when assoc_eq a (camlp5_assoc assoc) ->
-      None
+      DefaultLevel
   (* Otherwise, force the level, n or n-1, according to expected assoc *)
-  | (NumLevel n,BorderProd (Left,Some LeftA)) -> Some (Some n)
-  | ((NumLevel _ | DefaultLevel),BorderProd (Left,Some _)) -> Some None
+  | (NumLevel n,BorderProd (Left,Some LeftA)) -> NumLevel n
+  | ((NumLevel _ | DefaultLevel),BorderProd (Left,Some _)) -> NextLevel
   (* None means NEXT *)
-  | (NextLevel,_) -> assert (Notation.notation_entry_eq custom custom'); 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)
+    if from = n + 1 then NextLevel else NumLevel n
 
 type _ target =
 | ForConstr : constr_expr target
@@ -350,9 +347,9 @@ let symbol_of_target : type s. _ -> _ -> _ -> _ -> s target -> (s, s) mayrec_sym
     let g = target_entry custom forpat 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) -> 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
-- 
cgit v1.2.3


From 6eb4dbf6ba77ae7e9087832ea1e27426b515a8e8 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Mon, 10 Feb 2020 18:54:55 +0100
Subject: Custom entries: accept that no level is mentioned for a subentry.

If it is for an internal non-terminal then:
- if for a subentry different from constr, it refers to the head of
  the subentry
- if in constr, it is 200 by convention

If it is on the border of a rule, then:
- if it is in a subentry different from the entry it lives, it refers
  to the head of the subentry (or 200 by convention if in constr)
- if it is in the same entry, the rule for associativity tells if a
  SELF, a NEXT, or (if on the right) a LEVEL
---
 doc/sphinx/user-extensions/syntax-extensions.rst | 8 +++++++-
 vernac/egramcoq.ml                               | 3 ++-
 vernac/metasyntax.ml                             | 9 ++-------
 3 files changed, 11 insertions(+), 9 deletions(-)

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/vernac/egramcoq.ml b/vernac/egramcoq.ml
index bf49fb4df5..9f41287bce 100644
--- a/vernac/egramcoq.ml
+++ b/vernac/egramcoq.ml
@@ -213,7 +213,8 @@ let adjust_level custom assoc (custom',from) p = let open Gramlib.Gramext in mat
 (* 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') -> 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)) -> NumLevel n
   | (DefaultLevel,BorderProd (_,None)) -> assert false
diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml
index 1e46d35ed7..7794b0a37a 100644
--- a/vernac/metasyntax.ml
+++ b/vernac/metasyntax.ml
@@ -978,17 +978,12 @@ let is_only_printing mods =
 let set_entry_type from n etyps (x,typ) =
   let make_lev n s = match typ with
     | BorderProd _ -> NumLevel n
-    | InternalProd ->
-      if s = InConstrEntry then NumLevel 200 else
-      user_err (strbrk "level of inner subentry " ++ quote (pr_notation_entry s) ++
-                str " cannot be inferred. It must be given explicitly.") in
+    | InternalProd -> DefaultLevel in
   let typ = try
     match List.assoc x etyps, typ with
       | ETConstr (s,bko,DefaultLevel), _ ->
          if notation_entry_eq from s then ETConstr (s,bko,(make_lev n s,typ))
-         else if s = InConstrEntry then ETConstr (s,bko,(make_lev 200 s,typ)) else
-         user_err (strbrk "level of subentry " ++ quote (pr_notation_entry s) ++
-                   str " cannot be inferred. It must be given explicitly.")
+         else ETConstr (s,bko,(DefaultLevel,typ))
       | ETConstr (s,bko,n), BorderProd (left,_) ->
           ETConstr (s,bko,(n,BorderProd (left,None)))
       | ETConstr (s,bko,n), InternalProd ->
-- 
cgit v1.2.3


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


From 9970ee1b131cb7e3b891d8258e492caafca46158 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sat, 15 Feb 2020 19:11:56 +0100
Subject: Fixing bug #9521 (anomaly due to missing declaration of level in
 custom entry).

This fixes also #9640 part 1.
---
 test-suite/bugs/closed/bug_9521.v | 23 +++++++++++++++++++++++
 test-suite/bugs/closed/bug_9640.v | 23 +++++++++++++++++++++++
 vernac/egramcoq.ml                |  7 ++++++-
 3 files changed, 52 insertions(+), 1 deletion(-)
 create mode 100644 test-suite/bugs/closed/bug_9521.v
 create mode 100644 test-suite/bugs/closed/bug_9640.v

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/vernac/egramcoq.ml b/vernac/egramcoq.ml
index 9f41287bce..3181bcc4bc 100644
--- a/vernac/egramcoq.ml
+++ b/vernac/egramcoq.ml
@@ -507,13 +507,18 @@ let prepare_empty_levels forpat (where,(pos,p4assoc,name,reinit)) =
   let empty = (pos, [(name, p4assoc, [])]) in
   ExtendRule (target_entry where forpat, reinit, empty)
 
+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' assoc from forpat level rem in
    let push where p rem =
      match symbol_of_target where p assoc from forpat with
-     | MayRecNo (Aentryl (_,i)) when level <> Some (int_of_string i) -> (where,int_of_string i) :: rem
+     | 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
-- 
cgit v1.2.3


From acde8140bd51be112be33ae07db68b2f3b93302c Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Thu, 2 Jan 2020 20:02:38 +0100
Subject: Adding change log.

---
 .../11530-master+fix11331-custom-entries-precedence.rst           | 8 ++++++++
 1 file changed, 8 insertions(+)
 create mode 100644 doc/changelog/03-notations/11530-master+fix11331-custom-entries-precedence.rst

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>`_).
-- 
cgit v1.2.3


From 29919b725262dca76708192bde65ce82860747be Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Mon, 10 Feb 2020 22:31:55 +0100
Subject: Granting #9516 and #9518 (support for numerals and strings in custom
 entries).

---
 interp/constrextern.ml           |  8 +++++---
 interp/notation.ml               | 28 ++++++++++++++++++++++++++++
 interp/notation.mli              |  3 +++
 parsing/extend.ml                |  2 ++
 parsing/notgram_ops.ml           |  3 ++-
 test-suite/output/Notations4.out |  2 ++
 test-suite/output/Notations4.v   |  3 +++
 vernac/egramcoq.ml               |  8 ++++++++
 vernac/g_vernac.mlg              |  1 +
 vernac/metasyntax.ml             | 17 ++++++++++++-----
 vernac/ppvernac.ml               |  1 +
 11 files changed, 67 insertions(+), 9 deletions(-)

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 848861238a..178f7354f2 100644
--- a/parsing/extend.ml
+++ b/parsing/extend.ml
@@ -29,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 *)
@@ -53,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 a5ade43295..5c220abeda 100644
--- a/parsing/notgram_ops.ml
+++ b/parsing/notgram_ops.ml
@@ -55,11 +55,12 @@ 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/output/Notations4.out b/test-suite/output/Notations4.out
index 807914a671..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}]
diff --git a/test-suite/output/Notations4.v b/test-suite/output/Notations4.v
index 2906698386..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.
diff --git a/vernac/egramcoq.ml b/vernac/egramcoq.ml
index 3181bcc4bc..5e98f5ddc0 100644
--- a/vernac/egramcoq.ml
+++ b/vernac/egramcoq.ml
@@ -249,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
@@ -369,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))
@@ -414,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))
diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg
index 28b9fa7449..97c9d23c68 100644
--- a/vernac/g_vernac.mlg
+++ b/vernac/g_vernac.mlg
@@ -1234,6 +1234,7 @@ GRAMMAR EXTEND Gram
   syntax_extension_type:
     [ [ IDENT "ident" -> { ETIdent } | IDENT "global" -> { ETGlobal }
       | IDENT "bigint" -> { ETBigint }
+      | IDENT "string" -> { ETString }
       | IDENT "binder" -> { ETBinder true }
       | IDENT "constr" -> { ETConstr (InConstrEntry,None,DefaultLevel) }
       | IDENT "constr"; n = at_level_opt; b = OPT constr_as_binder_kind -> { ETConstr (InConstrEntry,b,n) }
diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml
index 7794b0a37a..d39ee60c25 100644
--- a/vernac/metasyntax.ml
+++ b/vernac/metasyntax.ml
@@ -396,7 +396,7 @@ let unparsing_metavar i from typs =
   let x = List.nth typs (i-1) 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)
@@ -686,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)
@@ -989,7 +990,7 @@ let set_entry_type from n etyps (x,typ) =
       | ETConstr (s,bko,n), InternalProd ->
           ETConstr (s,bko,(n,InternalProd))
       | ETPattern (b,n), _ -> ETPattern (b,n)
-      | (ETIdent | ETBigint | ETGlobal | ETBinder _ as x), _ -> x
+      | (ETIdent | ETBigint | ETString | ETGlobal | ETBinder _ as x), _ -> x
     with Not_found ->
       ETConstr (from,None,(make_lev n from,typ))
   in (x,typ)
@@ -1011,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 =
@@ -1033,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.")
@@ -1097,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]) ->
@@ -1108,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
@@ -1149,7 +1154,7 @@ let find_precedence custom lev etyps symbols onlyprint =
           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,_,(NumLevel _ | NextLevel)), s' when s = s' -> test ()
-        | (ETIdent | ETBigint | ETGlobal), _ ->
+        | (ETIdent | ETBigint | ETString | ETGlobal), _ ->
             begin match lev with
             | None ->
               ([Feedback.msg_info ?loc:None ,strbrk "Setting notation at level 0."],0)
@@ -1375,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
 
diff --git a/vernac/ppvernac.ml b/vernac/ppvernac.ml
index f4918caeff..0cf407619b 100644
--- a/vernac/ppvernac.ml
+++ b/vernac/ppvernac.ml
@@ -126,6 +126,7 @@ open Pputils
     | 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"
 
-- 
cgit v1.2.3


From 96e78e7e25d666f30a7c00e0288762e127690c67 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sat, 15 Feb 2020 08:49:53 +0100
Subject: Suite picking numeral notation

Ceci est une suite à numeral notation in custom entries, cherchant à
raffiner la compatibilité entre entrées. C'est mélangé avec le "pick"
précédent, et c'est en chantier.
---
 parsing/notgram_ops.ml         | 92 ++++++++++++++++++++++++------------------
 parsing/notgram_ops.mli        |  2 +-
 test-suite/output/Notations4.v | 14 +++++++
 vernac/metasyntax.ml           | 54 +++++--------------------
 4 files changed, 78 insertions(+), 84 deletions(-)

diff --git a/parsing/notgram_ops.ml b/parsing/notgram_ops.ml
index 5c220abeda..5c79ec2eba 100644
--- a/parsing/notgram_ops.ml
+++ b/parsing/notgram_ops.ml
@@ -13,22 +13,7 @@ open CErrors
 open Util
 open Notation
 open Notation_gram
-
-(* Uninterpreted notation levels *)
-
-let notation_level_map = Summary.ref ~name:"notation_level_map" NotationMap.empty
-
-let declare_notation_level ?(onlyprint=false) ntn level =
-  try
-    let (level,onlyprint) = NotationMap.find ntn !notation_level_map in
-    if not onlyprint then anomaly (str "Notation " ++ pr_notation ntn ++ str " is already assigned a level.")
-  with Not_found ->
-  notation_level_map := NotationMap.add ntn (level,onlyprint) !notation_level_map
-
-let level_of_notation ?(onlyprint=false) ntn =
-  let (level,onlyprint') = NotationMap.find ntn !notation_level_map in
-  if onlyprint' && not onlyprint then raise Not_found;
-  level
+open Constrexpr
 
 (**********************************************************************)
 (* Equality *)
@@ -40,34 +25,61 @@ let parenRelation_eq t1 t2 = match t1, t2 with
 | Prec l1, Prec l2 -> Int.equal l1 l2
 | _ -> false
 
-let production_position_eq pp1 pp2 = match (pp1,pp2) with
-| BorderProd (side1,assoc1), BorderProd (side2,assoc2) -> side1 = side2 && assoc1 = assoc2
-| InternalProd, InternalProd -> true
-| (BorderProd _ | InternalProd), _ -> false
-
-let production_level_eq l1 l2 = match (l1,l2) with
-| NextLevel, NextLevel -> true
-| NumLevel n1, NumLevel n2 -> Int.equal n1 n2
-| 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
+let constr_entry_key_compatible v1 v2 = match v1, v2 with
+| (ETGlobal | ETBigint | ETString), (ETGlobal | ETBigint | ETString) -> true
+| (ETIdent | ETBigint | ETString), ETIdent -> true
+| ETIdent, (ETBigint | 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
+| ETConstr (s1,bko1,_lev1), ETConstr (s2,bko2,_lev2) ->
+   notation_entry_eq s1 s2 && Option.equal (=) bko1 bko2
 | ETPattern (b1,n1), ETPattern (b2,n2) -> b1 = b2 && Option.equal Int.equal n1 n2
 | (ETIdent | ETGlobal | ETBigint | ETString | ETBinder _ | ETConstr _ | ETPattern _), _ -> false
 
-let level_eq_gen strict (s1, l1, t1, u1) (s2, l2, t2, u2) =
+let level_compatible (s1, l1, t1, u1) (s2, l2, t2, u2) =
   let tolerability_eq (i1, r1) (i2, r2) = Int.equal i1 i2 && parenRelation_eq r1 r2 in
-  let prod_eq (l1,pp1) (l2,pp2) =
-    not strict ||
-    (production_level_eq l1 l2 && production_position_eq pp1 pp2) in
   notation_entry_eq s1 s2 && Int.equal l1 l2 && List.equal tolerability_eq t1 t2
-  && List.equal (constr_entry_key_eq prod_eq) u1 u2
+  && List.equal constr_entry_key_compatible u1 u2
 
-let level_eq = level_eq_gen false
+(* Uninterpreted notation levels *)
+
+let pr_arg_level from (lev,typ) =
+  let pplev = function
+  | (n,L) when Int.equal n from -> str "at next level"
+  | (n,E) -> str "at level " ++ int n
+  | (n,L) -> str "at level below " ++ int n
+  | (n,Prec m) when Int.equal m n -> str "at level " ++ int n
+  | (n,_) -> str "Unknown level" in
+  Ppvernac.pr_set_entry_type (fun _ -> (*TO CHECK*) mt()) typ ++
+  (match typ with
+   | ETConstr _ | ETPattern _ -> spc () ++ pplev lev
+   | _ -> mt ())
+
+let pr_level ntn (from,fromlevel,args,typs) =
+  (match from with InConstrEntry -> mt () | InCustomEntry s -> str "in " ++ str s ++ spc()) ++
+  str "at level " ++ int fromlevel ++ spc () ++ str "with arguments" ++ spc() ++
+  prlist_with_sep pr_comma (pr_arg_level fromlevel) (List.combine args typs)
+
+let error_incompatible_level ntn oldprec prec =
+  user_err
+    (str "Notation " ++ pr_notation ntn ++ str " is already defined" ++ spc() ++
+    pr_level ntn oldprec ++
+    spc() ++ str "while it is now required to be" ++ spc() ++
+    pr_level ntn prec ++ str ".")
+
+let notation_level_map = Summary.ref ~name:"notation_level_map" NotationMap.empty
+
+let declare_notation_level ?(onlyprint=false) ntn prec =
+  let oldprecs =
+    try
+      let oldprecs = NotationMap.find ntn !notation_level_map in
+      let f (old,onlyprint) = not onlyprint && not (level_compatible prec old) in
+      match List.filter f oldprecs with
+      | (oldprec,_)::_ -> error_incompatible_level ntn oldprec prec
+      | [] -> oldprecs
+    with Not_found -> [] in
+  notation_level_map := NotationMap.add ntn ((prec,onlyprint)::oldprecs) !notation_level_map
+
+let level_of_notation ?(onlyprint=false) ntn =
+  let (level,onlyprint') = NotationMap.find ntn !notation_level_map in
+  if onlyprint' && not onlyprint then raise Not_found;
+  level
diff --git a/parsing/notgram_ops.mli b/parsing/notgram_ops.mli
index c31f4505e7..3185db8f26 100644
--- a/parsing/notgram_ops.mli
+++ b/parsing/notgram_ops.mli
@@ -12,7 +12,7 @@
 open Constrexpr
 open Notation_gram
 
-val level_eq : level -> level -> bool
+val level_compatible : level -> level -> bool
 
 (** {6 Declare and test the level of a (possibly uninterpreted) notation } *)
 
diff --git a/test-suite/output/Notations4.v b/test-suite/output/Notations4.v
index 4ab800c9ba..dbfa939230 100644
--- a/test-suite/output/Notations4.v
+++ b/test-suite/output/Notations4.v
@@ -25,6 +25,20 @@ Check [ << # 0 >> ].
 Notation "n" := n%nat (in custom myconstr at level 0, n bigint).
 Check [ 2 + 3 ].
 
+Module A1.
+  (* This is compatible with bigint *)
+  Notation "x" := x (in custom myconstr at level 0, x ident).
+  (* This is incompatible with ident *)
+  Fail Notation "x" := x (in custom myconstr at level 0, x global).
+End A1.
+
+Module A2.
+  (* This is compatible with bigint *)
+  Notation "x" := x (in custom myconstr at level 0, x global).
+  (* This is compatible with bigint and global *)
+  Notation "x" := x (in custom myconstr at level 0, x string).
+End A2.
+
 End A.
 
 Module B.
diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml
index d39ee60c25..c9ad71c2e8 100644
--- a/vernac/metasyntax.ml
+++ b/vernac/metasyntax.ml
@@ -744,30 +744,6 @@ let recompute_assoc typs = let open Gramlib.Gramext in
 (**************************************************************************)
 (* Registration of syntax extensions (parsing/printing, no interpretation)*)
 
-let pr_arg_level from (lev,typ) =
-  let pplev = function
-  | (n,L) when Int.equal n from -> str "at next level"
-  | (n,E) -> str "at level " ++ int n
-  | (n,L) -> str "at level below " ++ int n
-  | (n,Prec m) when Int.equal m n -> str "at level " ++ int n
-  | (n,_) -> str "Unknown level" in
-  Ppvernac.pr_set_entry_type (fun _ -> (*TO CHECK*) mt()) typ ++
-  (match typ with
-   | ETConstr _ | ETPattern _ -> spc () ++ pplev lev
-   | _ -> mt ())
-
-let pr_level ntn (from,fromlevel,args,typs) =
-  (match from with InConstrEntry -> mt () | InCustomEntry s -> str "in " ++ str s ++ spc()) ++
-  str "at level " ++ int fromlevel ++ spc () ++ str "with arguments" ++ spc() ++
-  prlist_with_sep pr_comma (pr_arg_level fromlevel) (List.combine args typs)
-
-let error_incompatible_level ntn oldprec prec =
-  user_err
-    (str "Notation " ++ pr_notation ntn ++ str " is already defined" ++ spc() ++
-    pr_level ntn oldprec ++
-    spc() ++ str "while it is now required to be" ++ spc() ++
-    pr_level ntn prec ++ str ".")
-
 let error_parsing_incompatible_level ntn ntn' oldprec prec =
   user_err
     (str "Notation " ++ pr_notation ntn ++ str " relies on a parsing rule for " ++ pr_notation ntn' ++ spc() ++
@@ -792,27 +768,21 @@ let check_and_extend_constr_grammar ntn rule =
     if notation_eq ntn ntn_for_grammar then raise Not_found;
     let prec = rule.notgram_level in
     let oldprec = Notgram_ops.level_of_notation ntn_for_grammar in
-    if not (Notgram_ops.level_eq prec oldprec) then error_parsing_incompatible_level ntn ntn_for_grammar oldprec prec;
-  with Not_found ->
+    if not (Notgram_ops.level_compatible prec oldprec) then error_parsing_incompatible_level ntn ntn_for_grammar oldprec prec;
+  with NoSyntaxRule ->
     Egramcoq.extend_constr_grammar rule
 
 let cache_one_syntax_extension se =
   let ntn = se.synext_notation in
   let prec = se.synext_level in
   let onlyprint = se.synext_notgram.notgram_onlyprinting in
-  try
-    let oldprec = Notgram_ops.level_of_notation ~onlyprint ntn in
-    if not (Notgram_ops.level_eq prec oldprec) then error_incompatible_level ntn oldprec prec;
-  with Not_found ->
-    begin
-      (* Reserve the notation level *)
-      Notgram_ops.declare_notation_level ntn prec ~onlyprint;
-      (* Declare the parsing rule *)
-      if not onlyprint then List.iter (check_and_extend_constr_grammar ntn) se.synext_notgram.notgram_rules;
-      (* Declare the notation rule *)
-      declare_notation_rule ntn
-        ~extra:se.synext_extra (se.synext_unparsing, let (_,lev,_,_) = prec in lev) se.synext_notgram
-    end
+  (* Reserve the notation level *)
+  Notgram_ops.declare_notation_level ntn prec ~onlyprint;
+  (* Declare the parsing rule *)
+  if not onlyprint then List.iter (check_and_extend_constr_grammar ntn) se.synext_notgram.notgram_rules;
+  (* Declare the notation rule *)
+  declare_notation_rule ntn
+    ~extra:se.synext_extra (se.synext_unparsing, let (_,lev,_,_) = prec in lev) se.synext_notgram
 
 let cache_syntax_extension (_, (_, sy)) =
   cache_one_syntax_extension sy
@@ -1182,7 +1152,7 @@ let find_precedence custom lev etyps symbols onlyprint =
 
 let check_curly_brackets_notation_exists () =
   try let _ = Notgram_ops.level_of_notation (InConstrEntrySomeLevel,"{ _ }") in ()
-  with Not_found ->
+  with NoSyntaxRule ->
     user_err Pp.(str "Notations involving patterns of the form \"{ _ }\" are treated \n\
 specially and require that the notation \"{ _ }\" is already reserved.")
 
@@ -1421,8 +1391,6 @@ let with_syntax_protection f x =
 (**********************************************************************)
 (* Recovering existing syntax                                         *)
 
-exception NoSyntaxRule
-
 let recover_notation_syntax ntn =
   try
     let prec = Notgram_ops.level_of_notation ~onlyprint:true ntn (* Be as little restrictive as possible *) in
@@ -1435,7 +1403,7 @@ let recover_notation_syntax ntn =
       synext_unparsing = pp_rule;
       synext_extra = pp_extra_rules;
     }
-  with Not_found ->
+  with Not_found | NoSyntaxRule ->
     raise NoSyntaxRule
 
 let recover_squash_syntax sy =
-- 
cgit v1.2.3


From 6a630e92a2c0972d78e724482c71b1f7f7232369 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sat, 15 Feb 2020 18:42:55 +0100
Subject: Revert "Suite picking numeral notation"

This reverts commit 03c48bb6943312e606b80b7af65b1ccb7122a386.
---
 parsing/notgram_ops.ml         | 92 ++++++++++++++++++------------------------
 parsing/notgram_ops.mli        |  2 +-
 test-suite/output/Notations4.v | 14 -------
 vernac/metasyntax.ml           | 54 ++++++++++++++++++++-----
 4 files changed, 84 insertions(+), 78 deletions(-)

diff --git a/parsing/notgram_ops.ml b/parsing/notgram_ops.ml
index 5c79ec2eba..5c220abeda 100644
--- a/parsing/notgram_ops.ml
+++ b/parsing/notgram_ops.ml
@@ -13,7 +13,22 @@ open CErrors
 open Util
 open Notation
 open Notation_gram
-open Constrexpr
+
+(* Uninterpreted notation levels *)
+
+let notation_level_map = Summary.ref ~name:"notation_level_map" NotationMap.empty
+
+let declare_notation_level ?(onlyprint=false) ntn level =
+  try
+    let (level,onlyprint) = NotationMap.find ntn !notation_level_map in
+    if not onlyprint then anomaly (str "Notation " ++ pr_notation ntn ++ str " is already assigned a level.")
+  with Not_found ->
+  notation_level_map := NotationMap.add ntn (level,onlyprint) !notation_level_map
+
+let level_of_notation ?(onlyprint=false) ntn =
+  let (level,onlyprint') = NotationMap.find ntn !notation_level_map in
+  if onlyprint' && not onlyprint then raise Not_found;
+  level
 
 (**********************************************************************)
 (* Equality *)
@@ -25,61 +40,34 @@ let parenRelation_eq t1 t2 = match t1, t2 with
 | Prec l1, Prec l2 -> Int.equal l1 l2
 | _ -> false
 
-let constr_entry_key_compatible v1 v2 = match v1, v2 with
-| (ETGlobal | ETBigint | ETString), (ETGlobal | ETBigint | ETString) -> true
-| (ETIdent | ETBigint | ETString), ETIdent -> true
-| ETIdent, (ETBigint | ETString) -> true
+let production_position_eq pp1 pp2 = match (pp1,pp2) with
+| BorderProd (side1,assoc1), BorderProd (side2,assoc2) -> side1 = side2 && assoc1 = assoc2
+| InternalProd, InternalProd -> true
+| (BorderProd _ | InternalProd), _ -> false
+
+let production_level_eq l1 l2 = match (l1,l2) with
+| NextLevel, NextLevel -> true
+| NumLevel n1, NumLevel n2 -> Int.equal n1 n2
+| 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 && Option.equal (=) bko1 bko2
+| 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 | ETString | ETBinder _ | ETConstr _ | ETPattern _), _ -> false
 
-let level_compatible (s1, l1, t1, u1) (s2, l2, t2, u2) =
+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
+  let prod_eq (l1,pp1) (l2,pp2) =
+    not strict ||
+    (production_level_eq l1 l2 && production_position_eq pp1 pp2) in
   notation_entry_eq s1 s2 && Int.equal l1 l2 && List.equal tolerability_eq t1 t2
-  && List.equal constr_entry_key_compatible u1 u2
+  && List.equal (constr_entry_key_eq prod_eq) u1 u2
 
-(* Uninterpreted notation levels *)
-
-let pr_arg_level from (lev,typ) =
-  let pplev = function
-  | (n,L) when Int.equal n from -> str "at next level"
-  | (n,E) -> str "at level " ++ int n
-  | (n,L) -> str "at level below " ++ int n
-  | (n,Prec m) when Int.equal m n -> str "at level " ++ int n
-  | (n,_) -> str "Unknown level" in
-  Ppvernac.pr_set_entry_type (fun _ -> (*TO CHECK*) mt()) typ ++
-  (match typ with
-   | ETConstr _ | ETPattern _ -> spc () ++ pplev lev
-   | _ -> mt ())
-
-let pr_level ntn (from,fromlevel,args,typs) =
-  (match from with InConstrEntry -> mt () | InCustomEntry s -> str "in " ++ str s ++ spc()) ++
-  str "at level " ++ int fromlevel ++ spc () ++ str "with arguments" ++ spc() ++
-  prlist_with_sep pr_comma (pr_arg_level fromlevel) (List.combine args typs)
-
-let error_incompatible_level ntn oldprec prec =
-  user_err
-    (str "Notation " ++ pr_notation ntn ++ str " is already defined" ++ spc() ++
-    pr_level ntn oldprec ++
-    spc() ++ str "while it is now required to be" ++ spc() ++
-    pr_level ntn prec ++ str ".")
-
-let notation_level_map = Summary.ref ~name:"notation_level_map" NotationMap.empty
-
-let declare_notation_level ?(onlyprint=false) ntn prec =
-  let oldprecs =
-    try
-      let oldprecs = NotationMap.find ntn !notation_level_map in
-      let f (old,onlyprint) = not onlyprint && not (level_compatible prec old) in
-      match List.filter f oldprecs with
-      | (oldprec,_)::_ -> error_incompatible_level ntn oldprec prec
-      | [] -> oldprecs
-    with Not_found -> [] in
-  notation_level_map := NotationMap.add ntn ((prec,onlyprint)::oldprecs) !notation_level_map
-
-let level_of_notation ?(onlyprint=false) ntn =
-  let (level,onlyprint') = NotationMap.find ntn !notation_level_map in
-  if onlyprint' && not onlyprint then raise Not_found;
-  level
+let level_eq = level_eq_gen false
diff --git a/parsing/notgram_ops.mli b/parsing/notgram_ops.mli
index 3185db8f26..c31f4505e7 100644
--- a/parsing/notgram_ops.mli
+++ b/parsing/notgram_ops.mli
@@ -12,7 +12,7 @@
 open Constrexpr
 open Notation_gram
 
-val level_compatible : level -> level -> bool
+val level_eq : level -> level -> bool
 
 (** {6 Declare and test the level of a (possibly uninterpreted) notation } *)
 
diff --git a/test-suite/output/Notations4.v b/test-suite/output/Notations4.v
index dbfa939230..4ab800c9ba 100644
--- a/test-suite/output/Notations4.v
+++ b/test-suite/output/Notations4.v
@@ -25,20 +25,6 @@ Check [ << # 0 >> ].
 Notation "n" := n%nat (in custom myconstr at level 0, n bigint).
 Check [ 2 + 3 ].
 
-Module A1.
-  (* This is compatible with bigint *)
-  Notation "x" := x (in custom myconstr at level 0, x ident).
-  (* This is incompatible with ident *)
-  Fail Notation "x" := x (in custom myconstr at level 0, x global).
-End A1.
-
-Module A2.
-  (* This is compatible with bigint *)
-  Notation "x" := x (in custom myconstr at level 0, x global).
-  (* This is compatible with bigint and global *)
-  Notation "x" := x (in custom myconstr at level 0, x string).
-End A2.
-
 End A.
 
 Module B.
diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml
index c9ad71c2e8..d39ee60c25 100644
--- a/vernac/metasyntax.ml
+++ b/vernac/metasyntax.ml
@@ -744,6 +744,30 @@ let recompute_assoc typs = let open Gramlib.Gramext in
 (**************************************************************************)
 (* Registration of syntax extensions (parsing/printing, no interpretation)*)
 
+let pr_arg_level from (lev,typ) =
+  let pplev = function
+  | (n,L) when Int.equal n from -> str "at next level"
+  | (n,E) -> str "at level " ++ int n
+  | (n,L) -> str "at level below " ++ int n
+  | (n,Prec m) when Int.equal m n -> str "at level " ++ int n
+  | (n,_) -> str "Unknown level" in
+  Ppvernac.pr_set_entry_type (fun _ -> (*TO CHECK*) mt()) typ ++
+  (match typ with
+   | ETConstr _ | ETPattern _ -> spc () ++ pplev lev
+   | _ -> mt ())
+
+let pr_level ntn (from,fromlevel,args,typs) =
+  (match from with InConstrEntry -> mt () | InCustomEntry s -> str "in " ++ str s ++ spc()) ++
+  str "at level " ++ int fromlevel ++ spc () ++ str "with arguments" ++ spc() ++
+  prlist_with_sep pr_comma (pr_arg_level fromlevel) (List.combine args typs)
+
+let error_incompatible_level ntn oldprec prec =
+  user_err
+    (str "Notation " ++ pr_notation ntn ++ str " is already defined" ++ spc() ++
+    pr_level ntn oldprec ++
+    spc() ++ str "while it is now required to be" ++ spc() ++
+    pr_level ntn prec ++ str ".")
+
 let error_parsing_incompatible_level ntn ntn' oldprec prec =
   user_err
     (str "Notation " ++ pr_notation ntn ++ str " relies on a parsing rule for " ++ pr_notation ntn' ++ spc() ++
@@ -768,21 +792,27 @@ let check_and_extend_constr_grammar ntn rule =
     if notation_eq ntn ntn_for_grammar then raise Not_found;
     let prec = rule.notgram_level in
     let oldprec = Notgram_ops.level_of_notation ntn_for_grammar in
-    if not (Notgram_ops.level_compatible prec oldprec) then error_parsing_incompatible_level ntn ntn_for_grammar oldprec prec;
-  with NoSyntaxRule ->
+    if not (Notgram_ops.level_eq prec oldprec) then error_parsing_incompatible_level ntn ntn_for_grammar oldprec prec;
+  with Not_found ->
     Egramcoq.extend_constr_grammar rule
 
 let cache_one_syntax_extension se =
   let ntn = se.synext_notation in
   let prec = se.synext_level in
   let onlyprint = se.synext_notgram.notgram_onlyprinting in
-  (* Reserve the notation level *)
-  Notgram_ops.declare_notation_level ntn prec ~onlyprint;
-  (* Declare the parsing rule *)
-  if not onlyprint then List.iter (check_and_extend_constr_grammar ntn) se.synext_notgram.notgram_rules;
-  (* Declare the notation rule *)
-  declare_notation_rule ntn
-    ~extra:se.synext_extra (se.synext_unparsing, let (_,lev,_,_) = prec in lev) se.synext_notgram
+  try
+    let oldprec = Notgram_ops.level_of_notation ~onlyprint ntn in
+    if not (Notgram_ops.level_eq prec oldprec) then error_incompatible_level ntn oldprec prec;
+  with Not_found ->
+    begin
+      (* Reserve the notation level *)
+      Notgram_ops.declare_notation_level ntn prec ~onlyprint;
+      (* Declare the parsing rule *)
+      if not onlyprint then List.iter (check_and_extend_constr_grammar ntn) se.synext_notgram.notgram_rules;
+      (* Declare the notation rule *)
+      declare_notation_rule ntn
+        ~extra:se.synext_extra (se.synext_unparsing, let (_,lev,_,_) = prec in lev) se.synext_notgram
+    end
 
 let cache_syntax_extension (_, (_, sy)) =
   cache_one_syntax_extension sy
@@ -1152,7 +1182,7 @@ let find_precedence custom lev etyps symbols onlyprint =
 
 let check_curly_brackets_notation_exists () =
   try let _ = Notgram_ops.level_of_notation (InConstrEntrySomeLevel,"{ _ }") in ()
-  with NoSyntaxRule ->
+  with Not_found ->
     user_err Pp.(str "Notations involving patterns of the form \"{ _ }\" are treated \n\
 specially and require that the notation \"{ _ }\" is already reserved.")
 
@@ -1391,6 +1421,8 @@ let with_syntax_protection f x =
 (**********************************************************************)
 (* Recovering existing syntax                                         *)
 
+exception NoSyntaxRule
+
 let recover_notation_syntax ntn =
   try
     let prec = Notgram_ops.level_of_notation ~onlyprint:true ntn (* Be as little restrictive as possible *) in
@@ -1403,7 +1435,7 @@ let recover_notation_syntax ntn =
       synext_unparsing = pp_rule;
       synext_extra = pp_extra_rules;
     }
-  with Not_found | NoSyntaxRule ->
+  with Not_found ->
     raise NoSyntaxRule
 
 let recover_squash_syntax sy =
-- 
cgit v1.2.3