Merge PR #916: Fixing notation bug 5608 involving { } and a slight restructuration

24 files changed, 217 insertions, 211 deletions

diff --git a/API/API.ml b/API/API.ml
index 1d7a4a4f46..c4bcef6f6c 100644
--- a/API/API.ml
+++ b/API/API.ml
@@ -169,7 +169,6 @@ module Stdarg = Stdarg
 module Genintern = Genintern
 module Constrexpr_ops = Constrexpr_ops
 module Notation_ops = Notation_ops
-module Ppextend = Ppextend
 module Notation = Notation
 module Dumpglob = Dumpglob
 (* module Syntax_def *)
diff --git a/API/API.mli b/API/API.mli
index 1262899c5f..e7a434634c 100644
--- a/API/API.mli
+++ b/API/API.mli
@@ -3184,6 +3184,10 @@ sig
                        | NCast of notation_constr * notation_constr Misctypes.cast_type
   type interpretation = (Names.Id.t * (subscopes * notation_var_instance_type)) list *
     notation_constr
+  type precedence = int
+  type parenRelation =
+    | L | E | Any | Prec of precedence
+  type tolerability = precedence * parenRelation
 end
 
 module Tactypes :
@@ -4179,16 +4183,6 @@ sig
                                                     'a -> Notation_term.notation_constr -> Glob_term.glob_constr
 end
 
-module Ppextend :
-sig
-
-  type precedence = int
-  type parenRelation =
-    | L | E | Any | Prec of precedence
-  type tolerability = precedence * parenRelation
-
-end
-
 module Notation :
 sig
   type cases_pattern_status = bool
@@ -4880,7 +4874,7 @@ sig
   val pr_with_comments : ?loc:Loc.t -> Pp.t -> Pp.t
   val pr_lident : Names.Id.t Loc.located -> Pp.t
   val pr_lname : Names.Name.t Loc.located -> Pp.t
-  val prec_less : int -> int * Ppextend.parenRelation -> bool
+  val prec_less : int -> int * Notation_term.parenRelation -> bool
   val pr_constr_expr : Constrexpr.constr_expr -> Pp.t
   val pr_lconstr_expr : Constrexpr.constr_expr -> Pp.t
   val pr_constr_pattern_expr : Constrexpr.constr_pattern_expr -> Pp.t
diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 54861ae4cc..e85415bed3 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -320,38 +320,6 @@ let drop_implicits_in_patt cst nb_expl args =
        let imps = List.skipn_at_least nb_expl (select_stronger_impargs impl_st) in
        impls_fit [] (imps,args)
 
-let has_curly_brackets ntn =
-  String.length ntn >= 6 && (String.is_sub "{ _ } " ntn 0 ||
-    String.is_sub " { _ }" ntn (String.length ntn - 6) ||
-    String.string_contains ~where:ntn ~what:" { _ } ")
-
-let rec wildcards ntn n =
-  if Int.equal n (String.length ntn) then []
-  else let l = spaces ntn (n+1) in if ntn.[n] == '_' then n::l else l
-and spaces ntn n =
-  if Int.equal n (String.length ntn) then []
-  else if ntn.[n] == ' ' then wildcards ntn (n+1) else spaces ntn (n+1)
-
-let expand_curly_brackets loc mknot ntn l =
-  let ntn' = ref ntn in
-  let rec expand_ntn i =
-    function
-    | [] -> []
-    | a::l ->
-        let a' =
-          let p = List.nth (wildcards !ntn' 0) i - 2 in
-          if p>=0 && p+5 <= String.length !ntn' && String.is_sub "{ _ }" !ntn' p
-          then begin
-            ntn' :=
-              String.sub !ntn' 0 p ^ "_" ^
-              String.sub !ntn' (p+5) (String.length !ntn' -p-5);
-            mknot (loc,"{ _ }",[a]) end
-          else a in
-        a' :: expand_ntn (i+1) l in
-  let l = expand_ntn 0 l in
-  (* side effect *)
-  mknot (loc,!ntn',l)
-
 let destPrim = function { CAst.v = CPrim t } -> Some t | _ -> None
 let destPatPrim = function { CAst.v = CPatPrim t } -> Some t | _ -> None
 
@@ -367,9 +335,7 @@ let is_zero s =
   in aux 0
 
 let make_notation_gen loc ntn mknot mkprim destprim l =
-  if has_curly_brackets ntn
-  then expand_curly_brackets loc mknot ntn l
-  else match ntn,List.map destprim l with
+  match ntn,List.map destprim l with
     (* Special case to avoid writing "- 3" for e.g. (Z.opp 3) *)
     | "- _", [Some (Numeral (p,true))] when not (is_zero p) ->
         mknot (loc,ntn,([mknot (loc,"( _ )",l)]))
diff --git a/interp/notation.ml b/interp/notation.ml
index c07a009438..c373faf680 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -41,7 +41,6 @@ open Context.Named.Declaration
 (**********************************************************************)
 (* Scope of symbols *)
 
-type level = precedence * tolerability list
 type delimiters = string
 type notation_location = (DirPath.t * DirPath.t) * string
 
@@ -83,11 +82,18 @@ let parenRelation_eq t1 t2 = match t1, t2 with
 | Prec l1, Prec l2 -> Int.equal l1 l2
 | _ -> false
 
-let level_eq (l1, t1) (l2, t2) =
+let notation_var_internalization_type_eq v1 v2 = match v1, v2 with
+| NtnInternTypeConstr, NtnInternTypeConstr -> true
+| NtnInternTypeBinder, NtnInternTypeBinder -> true
+| NtnInternTypeIdent, NtnInternTypeIdent -> true
+| (NtnInternTypeConstr | NtnInternTypeBinder | NtnInternTypeIdent), _ -> false
+
+let level_eq (l1, t1, u1) (l2, t2, u2) =
   let tolerability_eq (i1, r1) (i2, r2) =
     Int.equal i1 i2 && parenRelation_eq r1 r2
   in
   Int.equal l1 l2 && List.equal tolerability_eq t1 t2
+  && List.equal notation_var_internalization_type_eq u1 u2
 
 let declare_scope scope =
   try let _ = String.Map.find scope !scope_map in ()
diff --git a/interp/notation.mli b/interp/notation.mli
index e63ad10cde..f9f247fe10 100644
--- a/interp/notation.mli
+++ b/interp/notation.mli
@@ -21,7 +21,6 @@ open Ppextend
 (** A scope is a set of interpreters for symbols + optional
    interpreter and printers for integers + optional delimiters *)
 
-type level = precedence * tolerability list
 type delimiters = string
 type scope
 type scopes (** = [scope_name list] *)
diff --git a/interp/ppextend.ml b/interp/ppextend.ml
index 2bbe87bbca..3ebc9b71d2 100644
--- a/interp/ppextend.ml
+++ b/interp/ppextend.ml
@@ -7,17 +7,10 @@
 (************************************************************************)
 
 open Pp
+open Notation_term
 
 (*s Pretty-print. *)
 
-(* Dealing with precedences *)
-
-type precedence = int
-
-type parenRelation = L | E | Any | Prec of precedence
-
-type tolerability = precedence * parenRelation
-
 type ppbox =
   | PpHB of int
   | PpHOVB of int
diff --git a/interp/ppextend.mli b/interp/ppextend.mli
index a347a5c7b7..6ff5a42728 100644
--- a/interp/ppextend.mli
+++ b/interp/ppextend.mli
@@ -6,15 +6,9 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(** {6 Pretty-print. } *)
-
-(** Dealing with precedences *)
-
-type precedence = int
+open Notation_term
 
-type parenRelation = L | E | Any | Prec of precedence
-
-type tolerability = precedence * parenRelation
+(** {6 Pretty-print. } *)
 
 type ppbox =
   | PpHB of int
diff --git a/intf/notation_term.ml b/intf/notation_term.ml
index cee96040bd..c342da3dca 100644
--- a/intf/notation_term.ml
+++ b/intf/notation_term.ml
@@ -88,11 +88,24 @@ type grammar_constr_prod_item =
        concat with last parsed list when true; additionally release
        the p last items as if they were parsed autonomously *)
 
-type notation_grammar = {
-  notgram_level : int;
+(** Dealing with precedences *)
+
+type precedence = int
+type parenRelation = L | E | Any | Prec of precedence
+type tolerability = precedence * parenRelation
+
+type level = precedence * tolerability list * notation_var_internalization_type list
+
+(** Grammar rules for a notation *)
+
+type one_notation_grammar = {
+  notgram_level : level;
   notgram_assoc : Extend.gram_assoc option;
   notgram_notation : Constrexpr.notation;
   notgram_prods : grammar_constr_prod_item list list;
-  notgram_typs : notation_var_internalization_type list;
+}
+
+type notation_grammar = {
   notgram_onlyprinting : bool;
+  notgram_rules : one_notation_grammar list
 }
diff --git a/parsing/egramcoq.ml b/parsing/egramcoq.ml
index ec422c58db..870137ca11 100644
--- a/parsing/egramcoq.ml
+++ b/parsing/egramcoq.ml
@@ -443,7 +443,7 @@ let make_act : type r. r target -> _ -> r gen_eval = function
   CAst.make ~loc @@ CPatNotation (notation, env, [])
 
 let extend_constr state forpat ng =
-  let n = ng.notgram_level in
+  let n,_,_ = ng.notgram_level in
   let assoc = ng.notgram_assoc in
   let (entry, level) = interp_constr_entry_key forpat n in
   let fold (accu, state) pt =
@@ -464,7 +464,7 @@ let extend_constr state forpat ng =
 
 let constr_levels = GramState.field ()
 
-let extend_constr_notation (_, ng) state =
+let extend_constr_notation ng state =
   let levels = match GramState.get state constr_levels with
   | None -> default_constr_levels
   | Some lev -> lev
@@ -476,7 +476,7 @@ let extend_constr_notation (_, ng) state =
   let state = GramState.set state constr_levels levels in
   (r @ r', state)
 
-let constr_grammar : (Notation.level * notation_grammar) grammar_command =
+let constr_grammar : one_notation_grammar grammar_command =
   create_grammar_command "Notation" extend_constr_notation
 
-let extend_constr_grammar pr ntn = extend_grammar_command constr_grammar (pr, ntn)
+let extend_constr_grammar ntn = extend_grammar_command constr_grammar ntn
diff --git a/parsing/egramcoq.mli b/parsing/egramcoq.mli
index 248de3348e..8e0469275c 100644
--- a/parsing/egramcoq.mli
+++ b/parsing/egramcoq.mli
@@ -13,5 +13,5 @@
 
 (** {5 Adding notations} *)
 
-val extend_constr_grammar : Notation.level -> Notation_term.notation_grammar -> unit
+val extend_constr_grammar : Notation_term.one_notation_grammar -> unit
 (** Add a term notation rule to the parsing system. *)
diff --git a/plugins/ltac/extraargs.ml4 b/plugins/ltac/extraargs.ml4
index 6097951330..89feea8dcf 100644
--- a/plugins/ltac/extraargs.ml4
+++ b/plugins/ltac/extraargs.ml4
@@ -249,7 +249,7 @@ END
 let pr_by_arg_tac _prc _prlc prtac opt_c =
   match opt_c with
     | None -> mt ()
-    | Some t -> hov 2 (str "by" ++ spc () ++ prtac (3,Ppextend.E) t)
+    | Some t -> hov 2 (str "by" ++ spc () ++ prtac (3,Notation_term.E) t)
 
 ARGUMENT EXTEND by_arg_tac
   TYPED AS tactic_opt
diff --git a/plugins/ltac/extraargs.mli b/plugins/ltac/extraargs.mli
index b06f35ddc4..00668ddc7d 100644
--- a/plugins/ltac/extraargs.mli
+++ b/plugins/ltac/extraargs.mli
@@ -64,7 +64,7 @@ val wit_by_arg_tac :
   Geninterp.Val.t option) Genarg.genarg_type
 
 val pr_by_arg_tac : 
-  (int * Ppextend.parenRelation -> raw_tactic_expr -> Pp.t) ->
+  (int * Notation_term.parenRelation -> raw_tactic_expr -> Pp.t) ->
   raw_tactic_expr option -> Pp.t
 
 val test_lpar_id_colon : unit Pcoq.Gram.entry
diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml
index 140cc33440..cb7d9b9c02 100644
--- a/plugins/ltac/pptactic.ml
+++ b/plugins/ltac/pptactic.ml
@@ -18,7 +18,7 @@ open Geninterp
 open Stdarg
 open Tacarg
 open Libnames
-open Ppextend
+open Notation_term
 open Misctypes
 open Locus
 open Decl_kinds
diff --git a/plugins/ltac/pptactic.mli b/plugins/ltac/pptactic.mli
index 0bf9bc7f62..1f6ebaf448 100644
--- a/plugins/ltac/pptactic.mli
+++ b/plugins/ltac/pptactic.mli
@@ -16,7 +16,7 @@ open Misctypes
 open Environ
 open Constrexpr
 open Tacexpr
-open Ppextend
+open Notation_term
 
 type 'a grammar_tactic_prod_item_expr =
 | TacTerm of string
diff --git a/plugins/ssr/ssrparser.ml4 b/plugins/ssr/ssrparser.ml4
index ce23bb2b30..db1981228a 100644
--- a/plugins/ssr/ssrparser.ml4
+++ b/plugins/ssr/ssrparser.ml4
@@ -62,7 +62,7 @@ DECLARE PLUGIN "ssreflect_plugin"
  * we thus save the lexer to restore it at the end of the file *)
 let frozen_lexer = CLexer.get_keyword_state () ;;
 
-let tacltop = (5,Ppextend.E)
+let tacltop = (5,Notation_term.E)
 
 let pr_ssrtacarg _ _ prt = prt tacltop
 ARGUMENT EXTEND ssrtacarg TYPED AS tactic PRINTED BY pr_ssrtacarg
diff --git a/plugins/ssr/ssrparser.mli b/plugins/ssr/ssrparser.mli
index 88beeaa711..f9dc345e15 100644
--- a/plugins/ssr/ssrparser.mli
+++ b/plugins/ssr/ssrparser.mli
@@ -10,11 +10,11 @@
 
 val ssrtacarg : Tacexpr.raw_tactic_expr Pcoq.Gram.entry
 val wit_ssrtacarg : (Tacexpr.raw_tactic_expr, Tacexpr.glob_tactic_expr, Geninterp.Val.t) Genarg.genarg_type
-val pr_ssrtacarg : 'a -> 'b -> (int * Ppextend.parenRelation -> 'c) -> 'c
+val pr_ssrtacarg : 'a -> 'b -> (Notation_term.tolerability -> 'c) -> 'c
 
 val ssrtclarg : Tacexpr.raw_tactic_expr Pcoq.Gram.entry
 val wit_ssrtclarg : (Tacexpr.raw_tactic_expr, Tacexpr.glob_tactic_expr, Geninterp.Val.t) Genarg.genarg_type
-val pr_ssrtclarg : 'a -> 'b -> (int * Ppextend.parenRelation -> 'c -> 'd) -> 'c -> 'd
+val pr_ssrtclarg : 'a -> 'b -> (Notation_term.tolerability -> 'c -> 'd) -> 'c -> 'd
 
 val add_genarg : string -> ('a -> Pp.t) -> 'a Genarg.uniform_genarg_type
 
diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml
index ee03bc9007..4a103cdd23 100644
--- a/printing/ppconstr.ml
+++ b/printing/ppconstr.ml
@@ -15,6 +15,7 @@ open Nameops
 open Libnames
 open Pputils
 open Ppextend
+open Notation_term
 open Constrexpr
 open Constrexpr_ops
 open Decl_kinds
@@ -737,7 +738,7 @@ let tag_var = tag Tag.variable
     pr_lconstr_pattern_expr : constr_pattern_expr -> Pp.t
   }
 
-  type precedence =  Ppextend.precedence * Ppextend.parenRelation
+  type precedence =  Notation_term.precedence * Notation_term.parenRelation
   let modular_constr_pr = pr
   let rec fix rf x = rf (fix rf) x
   let pr = fix modular_constr_pr mt
diff --git a/printing/ppconstr.mli b/printing/ppconstr.mli
index 8335034851..7546c748d8 100644
--- a/printing/ppconstr.mli
+++ b/printing/ppconstr.mli
@@ -15,6 +15,7 @@ open Libnames
 open Constrexpr
 open Names
 open Misctypes
+open Notation_term
 
 val extract_lam_binders :
   constr_expr -> local_binder_expr list * constr_expr
@@ -24,7 +25,7 @@ val split_fix :
   int -> constr_expr -> constr_expr ->
   local_binder_expr list *  constr_expr * constr_expr
 
-val prec_less : int -> int * Ppextend.parenRelation -> bool
+val prec_less : precedence -> tolerability -> bool
 
 val pr_tight_coma : unit -> Pp.t
 
diff --git a/test-suite/bugs/closed/5469.v b/test-suite/bugs/closed/5469.v
deleted file mode 100644
index fce671c754..0000000000
--- a/test-suite/bugs/closed/5469.v
+++ /dev/null
@@ -1,3 +0,0 @@
-(* Some problems with the special treatment of curly braces *)
-
-Reserved Notation "'a' { x }" (at level 0, format "'a' { x }").
diff --git a/test-suite/bugs/closed/5608.v b/test-suite/bugs/closed/5608.v
new file mode 100644
index 0000000000..f02eae69c2
--- /dev/null
+++ b/test-suite/bugs/closed/5608.v
@@ -0,0 +1,33 @@
+Reserved Notation "'slet' x .. y := A 'in' b"
+  (at level 200, x binder, y binder, b at level 200, format "'slet'  x .. y  :=  A  'in' '//' b").
+Reserved Notation "T x [1] = { A } ; 'return' ( b0 , b1 , .. , b2 )"
+  (at level 200, format "T  x [1]  =  { A } ; '//' 'return'  ( b0 ,  b1 ,  .. ,  b2 )").
+
+Delimit Scope ctype_scope with ctype.
+Local Open Scope ctype_scope.
+Delimit Scope expr_scope with expr.
+Inductive base_type := TZ | TWord (logsz : nat).
+Inductive flat_type := Tbase (T : base_type) | Prod (A B : flat_type).
+Context {var : base_type -> Type}.
+Fixpoint interp_flat_type (interp_base_type : base_type -> Type) (t : 
+flat_type) :=
+  match t with
+  | Tbase t => interp_base_type t
+  | Prod x y => prod (interp_flat_type interp_base_type x) (interp_flat_type 
+interp_base_type y)
+  end.
+Inductive exprf : flat_type -> Type :=
+| Var {t} (v : var t) : exprf (Tbase t)
+| LetIn {tx} (ex : exprf tx) {tC} (eC : interp_flat_type var tx -> exprf tC) : 
+exprf tC
+| Pair {tx} (ex : exprf tx) {ty} (ey : exprf ty) : exprf (Prod tx ty).
+Global Arguments Var {_} _.
+Global Arguments LetIn {_} _ {_} _.
+Global Arguments Pair {_} _ {_} _.
+Notation "T x [1] = { A } ; 'return' ( b0 , b1 , .. , b2 )" := (LetIn (tx:=T) A 
+(fun x => Pair .. (Pair b0%expr b1%expr) .. b2%expr)) : expr_scope.
+Definition foo :=
+  (fun x3 =>
+     (LetIn (Var x3) (fun x18 : var TZ
+                      => (Pair (Var x18) (Var x18))))).
+Print foo.
diff --git a/test-suite/output/Notations3.out b/test-suite/output/Notations3.out
index a9ae74fd67..e5dbfcb4be 100644
--- a/test-suite/output/Notations3.out
+++ b/test-suite/output/Notations3.out
@@ -1,3 +1,5 @@
+{x : nat | x = 0} + {True /\ False} + {forall x : nat, x = 0}
+     : Set
 [<0, 2 >]
      : nat * nat * (nat * nat)
 [<0, 2 >]
@@ -109,9 +111,14 @@ fun x : ?A => x === x
      : forall x : ?A, x = x
 where
 ?A : [x : ?A |- Type] (x cannot be used)
-{0, 1}
+{{0, 1}}
      : nat * nat
-{0, 1, 2}
+{{0, 1, 2}}
      : nat * (nat * nat)
-{0, 1, 2, 3}
+{{0, 1, 2, 3}}
      : nat * (nat * (nat * nat))
+letpair x [1] = {0};
+return (1, 2, 3, 4)
+     : nat * nat * nat * nat
+{{ 1 | 1 // 1 }}
+     : nat
diff --git a/test-suite/output/Notations3.v b/test-suite/output/Notations3.v
index dee0f70f79..b1015137d6 100644
--- a/test-suite/output/Notations3.v
+++ b/test-suite/output/Notations3.v
@@ -1,4 +1,9 @@
 (**********************************************************************)
+(* Check precedence, spacing, etc. in printing with curly brackets    *)
+
+Check {x|x=0}+{True/\False}+{forall x, x=0}.
+
+(**********************************************************************)
 (* Check printing of notations with several instances of a recursive pattern *)
 (* Was wrong but I could not trigger a problem due to the collision between *)
 (* different instances of ".." *)
@@ -161,10 +166,23 @@ End Bug4765.
 Notation "x === x" := (eq_refl x) (only printing, at level 10).
 Check (fun x => eq_refl x).
 
-(**********************************************************************)
 (* Test recursive notations with the recursive pattern repeated on the right *)
 
-Notation "{ x , .. , y , z }" := (pair x .. (pair y z) ..).
-Check {0,1}.
-Check {0,1,2}.
-Check {0,1,2,3}.
+Notation "{{ x , .. , y , z }}" := (pair x .. (pair y z) ..).
+Check {{0,1}}.
+Check {{0,1,2}}.
+Check {{0,1,2,3}}.
+
+(* Test printing of #5608                                             *)
+
+Reserved Notation "'letpair' x [1] = { A } ; 'return' ( b0 , b1 , .. , b2 )"
+  (at level 200, format "'letpair'  x  [1]  =  { A } ; '//' 'return'  ( b0 ,  b1 ,  .. ,  b2 )").
+Notation "'letpair' x [1] = { a } ; 'return' ( b0 , b1 , .. , b2 )" :=
+  (let x:=a in ( .. (b0,b1) .., b2)).
+Check letpair x [1] = {0}; return (1,2,3,4).
+
+(* Test spacing in #5569 *)
+
+Notation "{ { xL | xR // xcut } }" := (xL+xR+xcut)
+  (at level 0, xR at level 39, format "{ {  xL  |  xR  //  xcut  } }").
+Check 1+1+1.
diff --git a/theories/Init/Notations.v b/theories/Init/Notations.v
index e67ae6a925..5e8d2faa58 100644
--- a/theories/Init/Notations.v
+++ b/theories/Init/Notations.v
@@ -66,6 +66,9 @@ Reserved Notation "{ x }" (at level 0, x at level 99).
 
 (** Notations for sigma-types or subsets *)
 
+Reserved Notation "{ A }  + { B }" (at level 50, left associativity).
+Reserved Notation "A + { B }" (at level 50, left associativity).
+
 Reserved Notation "{ x  |  P }" (at level 0, x at level 99).
 Reserved Notation "{ x  |  P  & Q }" (at level 0, x at level 99).
 
diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml
index c0974d0a7c..8b042a3ca3 100644
--- a/vernac/metasyntax.ml
+++ b/vernac/metasyntax.ml
@@ -522,35 +522,11 @@ let read_recursive_format sl fmt =
   let slfmt, fmt = get_head fmt in
   slfmt, get_tail (slfmt, fmt)
 
-let warn_skip_spaces_curly =
-  CWarnings.create ~name:"skip-spaces-curly" ~category:"parsing"
-      (fun () ->strbrk "Skipping spaces inside curly brackets")
-
-let rec drop_spacing = function
-  | UnpCut _ :: fmt -> warn_skip_spaces_curly (); drop_spacing fmt
-  | UnpTerminal s' :: fmt when String.equal s' (String.make (String.length s') ' ') -> warn_skip_spaces_curly (); drop_spacing fmt
-  | fmt -> fmt
-
-let has_closing_curly_brace symbs fmt =
-  (* TODO: recognize and fail in case a box overlaps a pair of curly braces *)
-  let fmt = drop_spacing fmt in
-  match symbs, fmt with
-  | NonTerminal s :: symbs, (UnpTerminal s' as u) :: fmt when Id.equal s (Id.of_string s') ->
-     let fmt = drop_spacing fmt in
-     (match fmt with
-     | UnpTerminal "}" :: fmt -> Some (u :: fmt)
-     | _ -> None)
-  | _ -> None
-
 let hunks_of_format (from,(vars,typs)) symfmt =
-  let a = ref None in
   let rec aux = function
   | symbs, (UnpTerminal s' as u) :: fmt
       when String.equal s' (String.make (String.length s') ' ') ->
       let symbs, l = aux (symbs,fmt) in symbs, u :: l
-  | symbs, (UnpTerminal "{") :: fmt when (a := has_closing_curly_brace symbs fmt; !a <> None) ->
-      let newfmt = Option.get !a in
-      aux (symbs,newfmt)
   | Terminal s :: symbs, (UnpTerminal s') :: fmt
       when String.equal s (String.drop_simple_quotes s') ->
       let symbs, l = aux (symbs,fmt) in symbs, UnpTerminal s :: l
@@ -705,26 +681,40 @@ let recompute_assoc typs =
 (**************************************************************************)
 (* Registration of syntax extensions (parsing/printing, no interpretation)*)
 
-let pr_arg_level from = function
+let pr_arg_level from (lev,typ) =
+  let pplev = match lev with
   | (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"
-
-let pr_level ntn (from,args) =
+  | (n,_) -> str "Unknown level" in
+  let pptyp = match typ with
+  | NtnInternTypeConstr -> mt ()
+  | NtnInternTypeBinder -> str " " ++ surround (str "binder")
+  | NtnInternTypeIdent -> str " " ++ surround (str "ident") in
+  pplev ++ pptyp
+
+let pr_level ntn (from,args,typs) =
   str "at level " ++ int from ++ spc () ++ str "with arguments" ++ spc() ++
-  prlist_with_sep pr_comma (pr_arg_level from) args
+  prlist_with_sep pr_comma (pr_arg_level from) (List.combine args typs)
 
 let error_incompatible_level ntn oldprec prec =
   user_err 
-    (str "Notation " ++ str ntn ++ str " is already defined" ++ spc() ++
+    (str "Notation " ++ qstring 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 " ++ qstring ntn ++ str " relies on a parsing rule for " ++ qstring ntn' ++ spc() ++
+    str " which is already defined" ++ spc() ++
     pr_level ntn oldprec ++
     spc() ++ str "while it is now required to be" ++ spc() ++
     pr_level ntn prec ++ str ".")
 
 type syntax_extension = {
-  synext_level : Notation.level;
+  synext_level : Notation_term.level;
   synext_notation : notation;
   synext_notgram : notation_grammar;
   synext_unparsing : unparsing list;
@@ -736,7 +726,17 @@ let is_active_compat = function
 | None -> true
 | Some v -> 0 <= Flags.version_compare v !Flags.compat_version
 
-type syntax_extension_obj = locality_flag * syntax_extension list
+type syntax_extension_obj = locality_flag * syntax_extension
+
+let check_and_extend_constr_grammar ntn rule =
+  try
+    let ntn_for_grammar = rule.notgram_notation in
+    if String.equal ntn ntn_for_grammar then raise Not_found;
+    let prec = rule.notgram_level in
+    let oldprec = Notation.level_of_notation ntn_for_grammar in
+    if not (Notation.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
@@ -744,31 +744,30 @@ let cache_one_syntax_extension se =
   let onlyprint = se.synext_notgram.notgram_onlyprinting in
   try
     let oldprec = Notation.level_of_notation ntn in
-    if not (Notation.level_eq prec oldprec) then error_incompatible_level ntn oldprec prec
+    if not (Notation.level_eq prec oldprec) then error_incompatible_level ntn oldprec prec;
   with Not_found ->
     if is_active_compat se.synext_compat then begin
       (* Reserve the notation level *)
       Notation.declare_notation_level ntn prec;
       (* Declare the parsing rule *)
-      if not onlyprint then Egramcoq.extend_constr_grammar prec se.synext_notgram;
+      if not onlyprint then List.iter (check_and_extend_constr_grammar ntn) se.synext_notgram.notgram_rules;
       (* Declare the notation rule *)
       Notation.declare_notation_rule ntn
-        ~extra:se.synext_extra (se.synext_unparsing, fst prec) se.synext_notgram
+        ~extra:se.synext_extra (se.synext_unparsing, pi1 prec) se.synext_notgram
     end
 
 let cache_syntax_extension (_, (_, sy)) =
-  List.iter cache_one_syntax_extension sy
+  cache_one_syntax_extension sy
 
 let subst_parsing_rule subst x = x
 
 let subst_printing_rule subst x = x
 
 let subst_syntax_extension (subst, (local, sy)) =
-  let map sy = { sy with
-    synext_notgram = subst_parsing_rule subst sy.synext_notgram;
+  (local, { sy with
+    synext_notgram = { sy.synext_notgram with notgram_rules = List.map (subst_parsing_rule subst) sy.synext_notgram.notgram_rules };
     synext_unparsing = subst_printing_rule subst sy.synext_unparsing;
-  } in
-  (local, List.map map sy)
+  })
 
 let classify_syntax_definition (local, _ as o) =
   if local then Dispose else Substitute o
@@ -1049,13 +1048,10 @@ let remove_curly_brackets l =
   | Terminal "{" as t1 :: l ->
       let br,next = skip_break [] l in
       (match next with
-        | NonTerminal _ as x :: l' as l0 ->
+        | NonTerminal _ as x :: l' ->
             let br',next' = skip_break [] l' in
             (match next' with
-              | Terminal "}" as t2 :: l'' as l1 ->
-                 if not (List.equal Notation.symbol_eq l l0) ||
-		      not (List.equal Notation.symbol_eq l' l1) then
-		  warn_skip_spaces_curly ();
+              | Terminal "}" as t2 :: l'' ->
 		  if deb && List.is_empty l'' then [t1;x;t2] else begin
                     check_curly_brackets_notation_exists ();
                     x :: aux false l''
@@ -1067,6 +1063,8 @@ let remove_curly_brackets l =
 
 module SynData = struct
 
+  type subentry_types = (Id.t * (production_level, production_position) constr_entry_key_gen) list
+
   (* XXX: Document *)
   type syn_data = {
 
@@ -1089,17 +1087,28 @@ module SynData = struct
     intern_typs   : notation_var_internalization_type list;
 
     (* Notation data for parsing *)
-
-    level         : int;
-    syntax_data   : (Id.t * (production_level, production_position) constr_entry_key_gen) list * (* typs    *)
-                    symbol list;                                                                 (* symbols *)
+    level         : level;
+    pa_syntax_data : subentry_types * symbol list;
+    pp_syntax_data : subentry_types * symbol list;
     not_data      : notation *                   (* notation *)
-                    (int * parenRelation) list * (* precedence *)
+                    level *                      (* level, precedence, types *)
                     bool;                        (* needs_squash *)
   }
 
 end
 
+let find_subentry_types 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))
+      symbols in
+  let sy_typs = List.map (set_entry_type etyps) typs in
+  let prec = List.map (assoc_of_type n) sy_typs in
+  sy_typs, prec
+
 let compute_syntax_data df modifiers =
   let open SynData in
   let open NotationMods in
@@ -1115,27 +1124,24 @@ let compute_syntax_data df modifiers =
 
   (* Notations for interp and grammar  *)
   let ntn_for_interp = make_notation_key symbols in
-  let symbols' = remove_curly_brackets symbols in
-  let ntn_for_grammar = make_notation_key symbols' in
-  if not onlyprint then check_rule_productivity symbols';
-
-  (* Misc *)
-  let need_squash = not (List.equal Notation.symbol_eq symbols symbols') in
-  let msgs,n = find_precedence mods.level mods.etyps symbols' in
-  let innerlevel = NumLevel 200 in
-  let typs =
-    find_symbols
-      (NumLevel n,BorderProd(Left,assoc))
-      (innerlevel,InternalProd)
-      (NumLevel n,BorderProd(Right,assoc))
-      symbols' in
+  let symbols_for_grammar = remove_curly_brackets symbols in
+  let need_squash = not (List.equal Notation.symbol_eq symbols symbols_for_grammar) in
+  let ntn_for_grammar = if need_squash then make_notation_key symbols_for_grammar else ntn_for_interp in
+  if not onlyprint then check_rule_productivity symbols_for_grammar;
+  let msgs,n = find_precedence mods.level mods.etyps symbols in
   (* To globalize... *)
   let etyps = join_auxiliary_recursive_types recvars mods.etyps in
-  let sy_typs = List.map (set_entry_type etyps) typs in
-  let prec = List.map (assoc_of_type n) sy_typs in
+  let sy_typs, prec =
+    find_subentry_types n assoc etyps symbols in
+  let sy_typs_for_grammar, prec_for_grammar =
+    if need_squash then
+      find_subentry_types n assoc etyps symbols_for_grammar
+    else
+      sy_typs, prec in
   let i_typs = set_internalization_type sy_typs in
-  let sy_data = (sy_typs,symbols') in
-  let sy_fulldata = (ntn_for_grammar,prec,need_squash) in
+  let pa_sy_data = (sy_typs_for_grammar,symbols_for_grammar) in
+  let pp_sy_data = (sy_typs,symbols) in
+  let sy_fulldata = (ntn_for_grammar,(n,prec_for_grammar,i_typs),need_squash) in
   let df' = ((Lib.library_dp(),Lib.current_dirpath true),df) in
   let i_data = ntn_for_interp, df' in
 
@@ -1154,8 +1160,9 @@ let compute_syntax_data df modifiers =
     mainvars;
     intern_typs = i_typs;
 
-    level  = n;
-    syntax_data = sy_data;
+    level  = (n,prec,i_typs);
+    pa_syntax_data = pa_sy_data;
+    pp_syntax_data = pp_sy_data;
     not_data    = sy_fulldata;
   }
 
@@ -1236,25 +1243,9 @@ let with_syntax_protection f x =
 (**********************************************************************)
 (* Recovering existing syntax                                         *)
 
-let contract_notation ntn =
-  if String.equal ntn "{ _ }" then ntn else
-  let rec aux ntn i =
-    if i <= String.length ntn - 5 then
-      let ntn' =
-        if String.is_sub "{ _ }" ntn i &&
-           (i = 0 || ntn.[i-1] = ' ') &&
-           (i = String.length ntn - 5 || ntn.[i+5] = ' ')
-        then
-          String.sub ntn 0 i ^ "_" ^
-          String.sub ntn (i+5) (String.length ntn -i-5)
-        else ntn in
-      aux ntn' (i+1)
-    else ntn in
-  aux ntn 0
-
 exception NoSyntaxRule
 
-let recover_syntax ntn =
+let recover_notation_syntax ntn =
   try
     let prec = Notation.level_of_notation ntn in
     let pp_rule,_ = Notation.find_notation_printing_rule ntn in
@@ -1271,29 +1262,25 @@ let recover_syntax ntn =
     raise NoSyntaxRule
 
 let recover_squash_syntax sy =
-  let sq = recover_syntax "{ _ }" in
-  [sy; sq]
-
-let recover_notation_syntax rawntn =
-  let ntn = contract_notation rawntn in
-  let sy = recover_syntax ntn in
-  let need_squash = not (String.equal ntn rawntn) in
-  let rules = if need_squash then recover_squash_syntax sy else [sy] in
-  sy.synext_notgram.notgram_typs, rules, sy.synext_notgram.notgram_onlyprinting
+  let sq = recover_notation_syntax "{ _ }" in
+  sy :: sq.synext_notgram.notgram_rules
 
 (**********************************************************************)
 (* Main entry point for building parsing and printing rules           *)
 
-let make_pa_rule i_typs level (typs,symbols) ntn onlyprint =
+let make_pa_rule level (typs,symbols) ntn need_squash =
   let assoc = recompute_assoc typs in
   let prod = make_production typs symbols in
-  { notgram_level = level;
+  let sy = {
+    notgram_level = level;
     notgram_assoc = assoc;
     notgram_notation = ntn;
     notgram_prods = prod;
-    notgram_typs = i_typs;
-    notgram_onlyprinting = onlyprint;
-  }
+  } in
+  (* By construction, the rule for "{ _ }" is declared, but we need to
+     redeclare it because the file where it is declared needs not be open
+     when the current file opens (especially in presence of -nois) *)
+  if need_squash then recover_squash_syntax sy else [sy]
 
 let make_pp_rule level (typs,symbols) fmt =
   match fmt with
@@ -1302,21 +1289,16 @@ let make_pp_rule level (typs,symbols) fmt =
 
 (* let make_syntax_rules i_typs (ntn,prec,need_squash) sy_data fmt extra onlyprint compat = *)
 let make_syntax_rules (sd : SynData.syn_data) = let open SynData in
-  let ntn, prec, need_squash = sd.not_data in
-  let pa_rule = make_pa_rule sd.intern_typs sd.level sd.syntax_data ntn sd.only_printing in
-  let pp_rule = make_pp_rule sd.level sd.syntax_data sd.format in
-  let sy = {
-    synext_level    = (sd.level, prec);
-    synext_notation = ntn;
-    synext_notgram  = pa_rule;
+  let ntn_for_grammar, prec_for_grammar, need_squash = sd.not_data 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 (pi1 sd.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 };
     synext_unparsing = pp_rule;
     synext_extra  = sd.extra;
     synext_compat = sd.compat;
-  } in
-  (* By construction, the rule for "{ _ }" is declared, but we need to
-     redeclare it because the file where it is declared needs not be open
-     when the current file opens (especially in presence of -nois) *)
-  if need_squash then recover_squash_syntax sy else [sy]
+  }
 
 (**********************************************************************)
 (* Main functions about notations                                     *)
@@ -1361,11 +1343,11 @@ let add_notation_interpretation_core local df ?(impls=empty_internalization_env)
   let (recvars,mainvars,symbs) = analyze_notation_tokens ~onlyprint dfs in
   (* Recover types of variables and pa/pp rules; redeclare them if needed *)
   let i_typs, onlyprint = if not (is_numeral symbs) then begin
-    let i_typs,sy_rules,onlyprint' = recover_notation_syntax (make_notation_key symbs) in
-    let () = Lib.add_anonymous_leaf (inSyntaxExtension (local,sy_rules)) in
+    let sy = recover_notation_syntax (make_notation_key symbs) in
+    let () = Lib.add_anonymous_leaf (inSyntaxExtension (local,sy)) in
     (** If the only printing flag has been explicitly requested, put it back *)
-    let onlyprint = onlyprint || onlyprint' in
-    i_typs, onlyprint
+    let onlyprint = onlyprint || sy.synext_notgram.notgram_onlyprinting in
+    pi3 sy.synext_level, onlyprint
   end else [], false in
   (* Declare interpretation *)
   let path = (Lib.library_dp(), Lib.current_dirpath true) in