Réaffichage des Syntactic Definition (printer constr_expr).

Affinement de la gestion des niveaux de constr.
Cablage en dur du parsing et de l'affichage des délimiteurs de scopes.


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3295 85f007b7-540e-0410-9357-904b9bb8a0f7

20 files changed, 285 insertions, 234 deletions

diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index c813cf71d1..68bcd12357 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -26,6 +26,7 @@ open Topconstr
 open Rawterm
 open Pattern
 open Nametab
+open Symbols
 (*i*)
 
 (* Translation from rawconstr to front constr *)
@@ -285,7 +286,7 @@ and extern_numeral scopes t (sc,n) =
 
 and extern_symbol scopes t = function
   | [] -> raise No_match
-  | (sc,ntn,pat,n as rule)::rules ->
+  | (keyrule,pat,n as rule)::rules ->
       try
 	(* Adjusts to the number of arguments expected by the notation *)
 	let (t,args) = match t,n with
@@ -296,16 +297,21 @@ and extern_symbol scopes t = function
 	(* Try matching ... *)
 	let subst = match_aconstr t pat in
 	(* Try availability of interpretation ... *)
-	(match Symbols.availability_of_notation (sc,ntn) scopes with
-          (* Uninterpretation is not allowed in current context *)
-	  | None -> raise No_match
-          (* Uninterpretation is allowed in current context *)
-	  | Some scopt ->
-	      let scopes = option_cons scopt scopes in
-	      let l = List.map (fun (id,c) -> (id,extern scopes c)) subst in
-	      let e = insert_delimiters (CNotation (loc,ntn,l)) scopt in
-	      if args = [] then e 
-	      else explicitize [] e (List.map (extern scopes) args))
+        let e =
+          match keyrule with
+          | NotationRule (sc,ntn) ->
+	      (match Symbols.availability_of_notation (sc,ntn) scopes with
+                  (* Uninterpretation is not allowed in current context *)
+              | None -> raise No_match
+                  (* Uninterpretation is allowed in current context *)
+	      | Some scopt ->
+	          let scopes = option_cons scopt scopes in
+	          let l = list_map_assoc (extern scopes) subst in
+	          insert_delimiters (CNotation (loc,ntn,l)) scopt)
+          | SynDefRule kn ->
+              CRef (Qualid (loc, shortest_qualid_of_syndef kn)) in
+ 	if args = [] then e 
+	else explicitize [] e (List.map (extern scopes) args)
       with
 	  No_match -> extern_symbol scopes t rules
 
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 7236335c39..e8e42a7b4b 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -274,8 +274,8 @@ let rec intern_cases_pattern scopes aliases = function
   | CPatNumeral (loc, n) ->
       ([aliases],
       Symbols.interp_numeral_as_pattern loc n (alias_of aliases) scopes)
-  | CPatDelimiters (_, sc, e) ->
-      intern_cases_pattern (sc::scopes) aliases e
+  | CPatDelimiters (loc, key, e) ->
+      intern_cases_pattern (find_delimiters_scope loc key::scopes) aliases e
   | CPatAtom (loc, Some head) ->
       (match maybe_constructor head with
 	 | ConstrPat c ->
@@ -396,8 +396,8 @@ let internalise sigma env allow_soapp lvar c =
 	  (Symbols.interp_notation ntn scopes)
     | CNumeral (loc, n) ->
 	Symbols.interp_numeral loc n scopes
-    | CDelimiters (loc, sc, e) ->
-	intern (ids,impls,sc::scopes) e
+    | CDelimiters (loc, key, e) ->
+	intern (ids,impls,find_delimiters_scope loc key::scopes) e
     | CAppExpl (loc, ref, args) ->
         let (f,_,args_scopes) = intern_reference env lvar ref in
 	RApp (loc, f, intern_args env args_scopes args)
diff --git a/interp/symbols.ml b/interp/symbols.ml
index 87282f0467..0d949fb283 100644
--- a/interp/symbols.ml
+++ b/interp/symbols.ml
@@ -40,7 +40,7 @@ open Ppextend
 (* Scope of symbols *)
 
 type level = precedence * precedence list
-type delimiters = string * string
+type delimiters = string
 type scope = {
   notations: (aconstr * (level * string)) Stringmap.t;
   delimiters: delimiters option
@@ -86,19 +86,35 @@ let check_scope sc = let _ = find_scope sc in ()
 (**********************************************************************)
 (* Delimiters *)
 
-let declare_delimiters scope dlm =
-  let sc = find_scope scope in
-  if sc.delimiters <> None && Options.is_verbose () then
-    warning ("Overwriting previous delimiters in "^scope);
-  let sc = { sc with delimiters = Some dlm } in
-  scope_map := Stringmap.add scope sc !scope_map   
+let delimiters_map = ref Stringmap.empty
 
-let find_delimiters scope = (find_scope scope).delimiters
+let declare_delimiters scope key =
+  let sc = find_scope scope in
+  if sc.delimiters <> None && Options.is_verbose () then begin
+    let old = out_some sc.delimiters in
+    Options.if_verbose 
+      warning ("Overwritting previous delimiter key "^old^" in scope "^scope)
+  end;
+  let sc = { sc with delimiters = Some key } in
+  scope_map := Stringmap.add scope sc !scope_map;
+  if Stringmap.mem key !delimiters_map then begin
+    let oldsc = Stringmap.find key !delimiters_map in
+    Options.if_verbose warning ("Hidding binding of key "^key^" to "^oldsc)
+  end;
+  delimiters_map := Stringmap.add key scope !delimiters_map
+
+let find_delimiters_scope loc key = 
+  try Stringmap.find key !delimiters_map
+  with Not_found -> 
+    user_err_loc 
+    (loc, "find_delimiters", str ("Unknown scope delimiting key "^key))
 
 (* Uninterpretation tables *)
 
 type interpretation = identifier list * aconstr
-type interp_rule = scope_name * notation * interpretation * int option
+type interp_rule =
+  | NotationRule of scope_name * notation
+  | SynDefRule of kernel_name
 
 (* We define keys for rawterm and aconstr to split the syntax entries
    according to the key of the pattern (adapted from Chet Murthy by HH) *)
@@ -191,21 +207,17 @@ let rec find_without_delimiters find ntn_scope = function
 
 (* The mapping between notations and their interpretation *)
 
-let declare_interpretation ntn scope pat =
+let declare_notation_interpretation ntn scope (_,pat) prec df =
   let sc = find_scope scope in
   if Stringmap.mem ntn sc.notations && Options.is_verbose () then
     warning ("Notation "^ntn^" is already used in scope "^scope);
-  let sc = { sc with notations = Stringmap.add ntn pat sc.notations } in
+  let sc =
+    { sc with notations = Stringmap.add ntn (pat,(prec,df)) sc.notations } in
   scope_map := Stringmap.add scope sc !scope_map
 
-let declare_uninterpretation ntn scope metas c =
+let declare_uninterpretation rule (metas,c as pat) =
   let (key,n) = aconstr_key c in
-  notations_key_table :=
-    Gmapl.add key (scope,ntn,(metas,c),n) !notations_key_table
-
-let declare_notation ntn scope (metas,c) prec df onlyparse =
-  declare_interpretation ntn scope (c,(prec,df));
-  if not onlyparse then declare_uninterpretation ntn scope metas c
+  notations_key_table := Gmapl.add key (rule,pat,n) !notations_key_table
 
 let rec find_interpretation f = function
   | scope::scopes ->
@@ -340,7 +352,7 @@ let find_arguments_scope r =
 
 let pr_delimiters_info = function
   | None -> str "No delimiters"
-  | Some (l,r) -> str "Delimiters are " ++ str l ++ str " and " ++ str r
+  | Some key -> str "Delimiting key is " ++ str key
 
 let rec rawconstr_of_aconstr () x =
   map_aconstr_with_binders_loc dummy_loc (fun id () -> (id,())) 
@@ -383,12 +395,13 @@ let find_notation_printing_rule ntn =
 (* Synchronisation with reset *)
 
 let freeze () =
- (!scope_map, !scope_stack, !arguments_scope,
+ (!scope_map, !scope_stack, !arguments_scope, !delimiters_map,
   !notations_key_table, !printing_rules)
 
-let unfreeze (scm,scs,asc,fkm,pprules) =
+let unfreeze (scm,scs,asc,dlm,fkm,pprules) =
   scope_map := scm;
   scope_stack := scs;
+  delimiters_map := dlm;
   arguments_scope := asc;
   notations_key_table := fkm;
   printing_rules := pprules
@@ -399,6 +412,7 @@ let init () =
   scope_stack := Stringmap.empty
   arguments_scope := Refmap.empty
 *)
+  delimiters_map := Stringmap.empty;
   notations_key_table := Gmapl.empty;
   printing_rules := Stringmap.empty
 
diff --git a/interp/symbols.mli b/interp/symbols.mli
index 466a2bb281..24a1388039 100644
--- a/interp/symbols.mli
+++ b/interp/symbols.mli
@@ -28,7 +28,7 @@ open Ppextend
    interpreter and printers for integers + optional delimiters *)
 
 type level = precedence * precedence list
-type delimiters = string * string
+type delimiters = string
 type scope
 type scopes = scope_name list
 
@@ -43,7 +43,7 @@ val open_scope : scope_name -> unit
 (* Declare delimiters for printing *)
 
 val declare_delimiters : scope_name -> delimiters -> unit
-val find_delimiters : scope_name -> delimiters option
+val find_delimiters_scope : loc -> delimiters -> scope_name
 
 (*s Declare and uses back and forth a numeral interpretation *)
 
@@ -80,15 +80,20 @@ val availability_of_numeral : scope_name -> scopes -> scope_name option option
 type interpretation = identifier list * aconstr
 
 (* Binds a notation in a given scope to an interpretation *)
-type interp_rule = scope_name * notation * interpretation * int option
-val declare_notation : notation -> scope_name -> interpretation -> level ->
-  string -> bool -> unit
+type interp_rule =
+  | NotationRule of scope_name * notation
+  | SynDefRule of kernel_name
+val declare_notation_interpretation : notation -> scope_name ->
+      interpretation -> level -> string -> unit
+
+val declare_uninterpretation : interp_rule -> interpretation -> unit
 
 (* Returns the interpretation bound to a notation *)
 val interp_notation : notation -> scopes -> aconstr
 
 (* Returns the possible notations for a given term *)
-val uninterp_notations : rawconstr -> interp_rule list
+val uninterp_notations : rawconstr ->
+      (interp_rule * interpretation * int option) list
 
 (* Test if a notation is available in the scopes *)
 (* context [scopes] if available, the result is not None; the first *)
diff --git a/interp/syntax_def.ml b/interp/syntax_def.ml
index a49352da37..eef20a7b16 100644
--- a/interp/syntax_def.ml
+++ b/interp/syntax_def.ml
@@ -31,23 +31,20 @@ let _ = Summary.declare_summary
 let add_syntax_constant kn c =
   syntax_table := KNmap.add kn c !syntax_table
 
-let cache_syntax_constant ((sp,kn),c) =
-  if Nametab.exists_cci sp then
-    errorlabstrm "cache_syntax_constant"
-      (pr_id (basename sp) ++ str " already exists");
-  add_syntax_constant kn c;
-  Nametab.push_syntactic_definition (Nametab.Until 1) sp kn
-
 let load_syntax_constant i ((sp,kn),c) =
   if Nametab.exists_cci sp then
     errorlabstrm "cache_syntax_constant"
       (pr_id (basename sp) ++ str " already exists");
   add_syntax_constant kn c;
-  Nametab.push_syntactic_definition (Nametab.Until i) sp kn
+  Nametab.push_syntactic_definition (Nametab.Until i) sp kn;
+  Symbols.declare_uninterpretation (Symbols.SynDefRule kn) ([],c)
 
 let open_syntax_constant i ((sp,kn),c) =
   Nametab.push_syntactic_definition (Nametab.Exactly i) sp kn
 
+let cache_syntax_constant d =
+  load_syntax_constant 1 d
+
 let subst_syntax_constant ((sp,kn),subst,c) =
   subst_aconstr subst c
 
diff --git a/interp/topconstr.ml b/interp/topconstr.ml
index 8173d3fc45..c548d820db 100644
--- a/interp/topconstr.ml
+++ b/interp/topconstr.ml
@@ -240,7 +240,7 @@ type cases_pattern_expr =
   | CPatCstr of loc * reference * cases_pattern_expr list
   | CPatAtom of loc * reference option
   | CPatNumeral of loc * Bignat.bigint
-  | CPatDelimiters of loc * scope_name * cases_pattern_expr
+  | CPatDelimiters of loc * string * cases_pattern_expr
 
 type constr_expr =
   | CRef of reference
@@ -263,7 +263,7 @@ type constr_expr =
   | CNotation of loc * notation * (identifier * constr_expr) list
   | CGrammar of loc * aconstr * (identifier * constr_expr) list
   | CNumeral of loc * Bignat.bigint
-  | CDelimiters of loc * scope_name * constr_expr
+  | CDelimiters of loc * string * constr_expr
   | CDynamic of loc * Dyn.t
 
 and fixpoint_expr = identifier * int * constr_expr * constr_expr
diff --git a/interp/topconstr.mli b/interp/topconstr.mli
index 85b05a4faa..272b5391b6 100644
--- a/interp/topconstr.mli
+++ b/interp/topconstr.mli
@@ -64,7 +64,7 @@ type cases_pattern_expr =
   | CPatCstr of loc * reference * cases_pattern_expr list
   | CPatAtom of loc * reference option
   | CPatNumeral of loc * Bignat.bigint
-  | CPatDelimiters of loc * scope_name * cases_pattern_expr
+  | CPatDelimiters of loc * string * cases_pattern_expr
 
 type constr_expr =
   | CRef of reference
@@ -87,7 +87,7 @@ type constr_expr =
   | CNotation of loc * notation * (identifier * constr_expr) list
   | CGrammar of loc * aconstr * (identifier * constr_expr) list
   | CNumeral of loc * Bignat.bigint
-  | CDelimiters of loc * scope_name * constr_expr
+  | CDelimiters of loc * string * constr_expr
   | CDynamic of loc * Dyn.t
 
 and fixpoint_expr = identifier * int * constr_expr * constr_expr
diff --git a/parsing/egrammar.ml b/parsing/egrammar.ml
index 17d9736211..6e8cfb05bf 100644
--- a/parsing/egrammar.ml
+++ b/parsing/egrammar.ml
@@ -41,14 +41,8 @@ let constr_level = function
   | 8 -> "top"
   | n -> string_of_int n
 
-let symbolic_level = function
-  | 9 -> "constr9", None
-  | 10 -> "lconstr", None
-  | 11 -> "pattern", None
-  | n -> "constr", Some n
-
 let numeric_levels =
-  ref [8,Some Gramext.RightA; 1,None; 0,None ]
+  ref [8,Some Gramext.RightA; 1,Some Gramext.RightA; 0,Some Gramext.RightA]
 
 exception Found of Gramext.g_assoc option
 
@@ -110,7 +104,7 @@ let make_act f pil =
 	Gramext.action (fun loc -> f loc env)
     | None :: tl -> (* parse a non-binding item *)
         Gramext.action (fun _ -> make env tl)
-    | Some (p, (ETConstr _| ETOther _)) :: tl -> (* non-terminal *)
+    | Some (p, (ETConstr _| ETOther _)) :: tl -> (* constr non-terminal *)
         Gramext.action (fun (v:constr_expr) -> make ((p,v) :: env) tl)
     | Some (p, ETReference) :: tl -> (* non-terminal *)
         Gramext.action (fun (v:reference) -> make ((p,CRef v) :: env) tl)
@@ -142,25 +136,23 @@ let make_cases_pattern_act f pil =
  * annotations are added when type-checking the command, function
  * Extend.of_ast) *)
 
-let rec build_prod_item univ = function
-  | ProdList0 s -> Gramext.Slist0 (build_prod_item univ s)
-  | ProdList1 s -> Gramext.Slist1 (build_prod_item univ s)
-  | ProdOpt s   -> Gramext.Sopt   (build_prod_item univ s)
+let rec build_prod_item univ assoc = function
+  | ProdList0 s -> Gramext.Slist0 (build_prod_item univ assoc s)
+  | ProdList1 s -> Gramext.Slist1 (build_prod_item univ assoc s)
+  | ProdOpt s   -> Gramext.Sopt   (build_prod_item univ assoc s)
   | ProdPrimitive typ ->
-      match entry_of_type false typ with
-	| (eobj,None) ->
-	    Gramext.Snterm (Gram.Entry.obj eobj)
-	| (eobj,Some lev) ->
-	    Gramext.Snterml (Gram.Entry.obj eobj,constr_level lev)
+      match get_constr_production_entry assoc typ with
+	| (eobj,None) -> Gramext.Snterm (Gram.Entry.obj eobj)
+	| (eobj,Some lev) -> Gramext.Snterml (Gram.Entry.obj eobj,constr_level lev)
 
-let symbol_of_prod_item univ = function
+let symbol_of_prod_item univ assoc = function
   | Term tok -> (Gramext.Stoken tok, None)
   | NonTerm (nt, ovar) ->
-      let eobj = build_prod_item univ nt in
+      let eobj = build_prod_item univ assoc nt in
       (eobj, ovar)
 
-let make_rule univ etyp rule =
-  let pil = List.map (symbol_of_prod_item univ) rule.gr_production in
+let make_rule univ assoc etyp rule =
+  let pil = List.map (symbol_of_prod_item univ assoc) rule.gr_production in
   let (symbs,ntl) = List.split pil in
   let f loc env = match rule.gr_action, env with
     | AVar p, [p',a] when p=p' -> a
@@ -169,19 +161,26 @@ let make_rule univ etyp rule =
     | AApp (AVar f,[AVar a]), [a',w;f',v] when f=f' & a=a' ->
         CApp (loc,v,[w,None])
     | pat,_ -> CGrammar (loc, pat, env) in
-  let act = make_act f ntl in
+  let act = match etyp with
+    | ETPattern -> 
+        (* Ugly *)
+        let f loc env = match rule.gr_action, env with
+          | AVar p, [p',a] when p=p' -> a
+          | _ -> error "Unable to handle this grammar extension of pattern" in
+        make_cases_pattern_act f ntl
+    | _ -> make_act f ntl in
   (symbs, act)
 
 (* Rules of a level are entered in reverse order, so that the first rules
    are applied before the last ones *)
 let extend_entry univ (te, etyp, pos, name, ass, rls) =
-  let rules = List.rev (List.map (make_rule univ etyp) rls) in
+  let rules = List.rev (List.map (make_rule univ ass etyp) rls) in
   grammar_extend te pos [(name, ass, rules)]
 
 (* Defines new entries. If the entry already exists, check its type *)
 let define_entry univ {ge_name=n; gl_assoc=ass; gl_rules=rls} =
   let typ = explicitize_entry (fst univ) n in
-  let e,lev = entry_of_type true typ in
+  let e,lev = get_constr_entry typ in
   let pos,ass = find_position ass lev in
   let name = option_app constr_level lev in
   (e,typ,pos,name,ass,rls)
@@ -214,14 +213,14 @@ let make_gen_act f pil =
 
 let extend_constr entry pos (level,assoc) make_act pt =
   let univ = get_univ "constr" in
-  let pil = List.map (symbol_of_prod_item univ) pt in
+  let pil = List.map (symbol_of_prod_item univ assoc) pt in
   let (symbs,ntl) = List.split pil in
   let act = make_act ntl in
   grammar_extend entry pos [(level, assoc, [symbs, act])]
 
 let extend_constr_notation (n,assoc,ntn,rule) =
   let mkact loc env = CNotation (loc,ntn,env) in
-  let (e,level) = entry_of_type false (ETConstr ((n,Ppextend.E),Some n)) in
+  let (e,level) = get_constr_entry (ETConstr (n,())) in
   let pos,assoc = find_position assoc level in
   extend_constr e pos (option_app constr_level level,assoc) 
     (make_act mkact) rule
diff --git a/parsing/esyntax.ml b/parsing/esyntax.ml
index 859b5548a5..1fa8523628 100644
--- a/parsing/esyntax.ml
+++ b/parsing/esyntax.ml
@@ -186,9 +186,8 @@ let pr_parenthesis inherited se strm =
     
 let print_delimiters inh se strm = function
   | None -> pr_parenthesis inh se strm
-  | Some sc ->
-      let (left,right) = out_some (find_delimiters sc) in
-      assert (left <> "" && right <> "");
+  | Some key ->
+      let left = "`"^key^":" and right = "`" in
       let lspace =
 	if is_letter (left.[String.length left -1]) then str " " else mt () in
       let rspace =
diff --git a/parsing/extend.ml b/parsing/extend.ml
index 70704f0195..2cde3e24e9 100644
--- a/parsing/extend.ml
+++ b/parsing/extend.ml
@@ -19,21 +19,30 @@ open Topconstr
 open Genarg
 
 type entry_type = argument_type
-type constr_entry_type =
+
+type production_position =
+  | BorderProd of bool * Gramext.g_assoc option  (* true=left; false=right *)
+  | InternalProd
+
+type 'pos constr_entry_key =
   | ETIdent | ETReference
-  | ETConstr of (int * parenRelation) * int option
+  | ETConstr of (int * 'pos)
   | ETPattern
   | ETOther of string * string
 
+type constr_production_entry = production_position constr_entry_key
+type constr_entry = unit constr_entry_key
+
 type nonterm_prod =
   | ProdList0 of nonterm_prod
   | ProdList1 of nonterm_prod
   | ProdOpt of nonterm_prod
-  | ProdPrimitive of constr_entry_type
+  | ProdPrimitive of constr_production_entry
 
 type prod_item =
   | Term of Token.pattern
-  | NonTerm of nonterm_prod * (Names.identifier * constr_entry_type) option
+  | NonTerm of
+      nonterm_prod * (Names.identifier * constr_production_entry) option
 
 type grammar_rule = {
   gr_name : string; 
@@ -54,13 +63,13 @@ type grammar_associativity = Gramext.g_assoc option
 (**********************************************************************)
 (* Globalisation and type-checking of Grammar actions *)
 
-type entry_context = (identifier * constr_entry_type) list
+type entry_context = identifier list
 
 let ast_to_rawconstr = ref (fun _ _ -> AVar (id_of_string "Z"))
 let set_ast_to_rawconstr f = ast_to_rawconstr := f
 
-let act_of_ast env = function
-  | SimpleAction (loc,ConstrNode a) -> !ast_to_rawconstr env a
+let act_of_ast vars = function
+  | SimpleAction (loc,ConstrNode a) -> !ast_to_rawconstr vars a
   | SimpleAction (loc,CasesPatternNode a) -> 
       failwith "TODO:act_of_ast: cases_pattern"
   | CaseAction _ -> failwith "case/let not supported"
@@ -71,7 +80,7 @@ type syntax_modifier =
   | SetItemLevel of string list * int
   | SetLevel of int
   | SetAssoc of Gramext.g_assoc
-  | SetEntryType of string * constr_entry_type
+  | SetEntryType of string * constr_entry
   | SetOnlyParsing
 
 type nonterm =
@@ -147,53 +156,40 @@ let rename_command nt =
 
 (* This translates constr0, constr1, ... level into camlp4 levels of constr *)
 
-let explicitize_entry univ nt =
+let explicitize_prod_entry pos univ nt =
   if univ = "prim" & nt = "var" then ETIdent else
   if univ <> "constr" then ETOther (univ,nt) else
   match nt with
-  | "constr0" -> ETConstr ((0,E),Some 0)
-  | "constr1" -> ETConstr ((1,E),Some 1)
-  | "constr2" -> ETConstr ((2,E),Some 2)
-  | "constr3" -> ETConstr ((3,E),Some 3)
-  | "lassoc_constr4" -> ETConstr ((4,E),Some 4)
-  | "constr5" -> ETConstr ((5,E),Some 5)
-  | "constr6" -> ETConstr ((6,E),Some 6)
-  | "constr7" -> ETConstr ((7,E),Some 7)
-  | "constr8" | "constr" -> ETConstr ((8,E),Some 8)
-  | "constr9" -> ETConstr ((9,E),Some 9)
-  | "constr10" | "lconstr" -> ETConstr ((10,E),Some 10)
+  | "constr0" -> ETConstr (0,pos)
+  | "constr1" -> ETConstr (1,pos)
+  | "constr2" -> ETConstr (2,pos)
+  | "constr3" -> ETConstr (3,pos)
+  | "lassoc_constr4" -> ETConstr (4,pos)
+  | "constr5" -> ETConstr (5,pos)
+  | "constr6" -> ETConstr (6,pos)
+  | "constr7" -> ETConstr (7,pos)
+  | "constr8" | "constr" -> ETConstr (8,pos)
+  | "constr9" -> ETConstr (9,pos)
+  | "constr10" | "lconstr" -> ETConstr (10,pos)
   | "pattern" -> ETPattern
   | "ident" -> ETIdent
   | "global" -> ETReference
   | _ -> ETOther (univ,nt)
 
-(* This determines if a reference to constr_n is a reference to the level
-   below wrt associativity (to be translated in camlp4 into "constr" without 
-   level) or to another level (to be translated into "constr LEVEL n") *)
-
-let clever_explicitize_entry univ name from assoc pos =
-  match explicitize_entry univ name, explicitize_entry "" from, pos with
-    | ETConstr ((n,_ as s),_),ETConstr ((lev,_),_),Some start
-	when n = lev - 1 & assoc <> Some Gramext.LeftA & start
-	  or n = lev & assoc = Some Gramext.LeftA & start
-	  or n = lev & assoc = Some Gramext.RightA & not start
-	  or n = lev - 1 & assoc <> Some Gramext.RightA & not start
-	-> ETConstr (s, None)
-    | x,_,_ -> x
-
-let qualified_nterm current_univ from ass pos = function
+let explicitize_entry = explicitize_prod_entry ()
+
+let qualified_nterm current_univ pos = function
   | NtQual (univ, en) ->
-      let univ = rename_command univ in
-      clever_explicitize_entry univ (rename_command en) from ass pos
+      explicitize_prod_entry pos (rename_command univ) (rename_command en)
   | NtShort en ->
-      clever_explicitize_entry current_univ (rename_command en) from ass pos
+      explicitize_prod_entry pos current_univ (rename_command en)
 
 let check_entry check_entry_type = function
   | ETOther (u,n) -> check_entry_type (u,n)
   | _ -> ()
 
-let nterm loc (((check_entry_type,univ),lev,ass),pos) nont =
-  let typ = qualified_nterm univ lev ass pos nont in
+let nterm loc ((check_entry_type,univ),pos) nont =
+  let typ = qualified_nterm univ pos nont in
   check_entry check_entry_type typ;
   typ
 
@@ -201,22 +197,22 @@ let prod_item univ env = function
   | VTerm s -> env, Term (terminal s)
   | VNonTerm (loc, nt, Some p) ->
      let typ = nterm loc univ nt in
-      ((p, typ) :: env, NonTerm (ProdPrimitive typ, Some (p,typ)))
+      (p :: env, NonTerm (ProdPrimitive typ, Some (p,typ)))
   | VNonTerm (loc, nt, None) ->
       let typ = nterm loc univ nt in 
       env, NonTerm (ProdPrimitive typ, None)
 
-let rec prod_item_list univ penv pil start =
+let rec prod_item_list univ penv pil current_pos =
   match pil with
     | [] -> [], penv
     | pi :: pitl ->
-	let pos = if pitl=[] then Some false else start in
+	let pos = if pitl=[] then (BorderProd (true,None)) else current_pos in
 	let (env, pic) = prod_item (univ,pos) penv pi in
-	let (pictl, act_env) = prod_item_list univ env pitl None in
+	let (pictl, act_env) = prod_item_list univ env pitl InternalProd in
         (pic :: pictl, act_env)
 
 let gram_rule univ (name,pil,act) =
-  let (pilc, act_env) = prod_item_list univ [] pil (Some true) in
+  let (pilc, act_env) = prod_item_list univ [] pil (BorderProd (false,None)) in
   let a = to_act_check_vars act_env act in
   { gr_name = name; gr_production = pilc; gr_action = a }
 
@@ -224,7 +220,7 @@ let gram_entry univ (nt, ass, rl) =
   let name = rename_command nt in
   { ge_name = name;
     gl_assoc = ass;
-    gl_rules = List.map (gram_rule (univ,name,ass)) rl }
+    gl_rules = List.map (gram_rule univ) rl }
 
 let interp_grammar_command univ ge entryl =
   let univ = rename_command univ in
@@ -266,21 +262,12 @@ let rec subst_hunk subst_pat subst hunk = match hunk with
    highest precedence), and the child's one, follow the given
    relation. *)
 
-(*
-let compare_prec (a1,b1,c1) (a2,b2,c2) =
-  match (a1=a2),(b1=b2),(c1=c2) with
-    | true,true,true -> 0
-    | true,true,false -> c1-c2
-    | true,false,_ -> b1-b2
-    | false,_,_ -> a1-a2
-*)
 let compare_prec a1 a2 = a1-a2
 
 let tolerable_prec oparent_prec_reln child_prec =
   match oparent_prec_reln with
     | Some (pprec, L) -> (compare_prec child_prec pprec) < 0
     | Some (pprec, E) -> (compare_prec child_prec pprec) <= 0
-    | Some (_, Prec level) -> (compare_prec child_prec level) <= 0
     | _ -> true
 
 type 'pat syntax_entry = {
diff --git a/parsing/extend.mli b/parsing/extend.mli
index 771434ea36..e55a417972 100644
--- a/parsing/extend.mli
+++ b/parsing/extend.mli
@@ -20,21 +20,30 @@ open Genarg
 (*i*)
 
 type entry_type = argument_type
-type constr_entry_type =
+
+type production_position =
+  | BorderProd of bool * Gramext.g_assoc option  (* true=left; false=right *)
+  | InternalProd
+
+type 'pos constr_entry_key =
   | ETIdent | ETReference
-  | ETConstr of (int * parenRelation) * int option
+  | ETConstr of (int * 'pos)
   | ETPattern
   | ETOther of string * string
 
+type constr_production_entry = production_position constr_entry_key
+type constr_entry = unit constr_entry_key
+
 type nonterm_prod =
   | ProdList0 of nonterm_prod
   | ProdList1 of nonterm_prod
   | ProdOpt of nonterm_prod
-  | ProdPrimitive of constr_entry_type
+  | ProdPrimitive of constr_production_entry
 
 type prod_item =
   | Term of Token.pattern
-  | NonTerm of nonterm_prod * (Names.identifier * constr_entry_type) option
+  | NonTerm of
+      nonterm_prod * (Names.identifier * constr_production_entry) option
 
 type grammar_rule = {
   gr_name : string; 
@@ -53,7 +62,7 @@ type grammar_command = {
 type grammar_associativity = Gramext.g_assoc option
 
 (* Globalisation and type-checking of Grammar actions *)
-type entry_context = (identifier * constr_entry_type) list
+type entry_context = identifier list
 val to_act_check_vars : entry_context -> grammar_action -> aconstr
 val set_ast_to_rawconstr : (entry_context -> constr_expr -> aconstr) -> unit
 
@@ -61,7 +70,7 @@ type syntax_modifier =
   | SetItemLevel of string list * int
   | SetLevel of int
   | SetAssoc of Gramext.g_assoc
-  | SetEntryType of string * constr_entry_type
+  | SetEntryType of string * constr_entry
   | SetOnlyParsing
 
 type nonterm =
@@ -77,7 +86,7 @@ val terminal : string -> string * string
 
 val rename_command : string -> string
 
-val explicitize_entry : string -> string -> constr_entry_type
+val explicitize_entry : string -> string -> constr_entry
 
 val subst_grammar_command : 
   Names.substitution -> grammar_command -> grammar_command
diff --git a/parsing/g_cases.ml4 b/parsing/g_cases.ml4
index a7b27de23d..7e1cf5da7a 100644
--- a/parsing/g_cases.ml4
+++ b/parsing/g_cases.ml4
@@ -28,10 +28,12 @@ GEXTEND Gram
       (* Hack to parse syntax "(n)" as a natural number *)
       | "("; G_constr.test_int_rparen; n = INT; ")" ->
 	  let n = CPatNumeral (loc,Bignat.POS (Bignat.of_string n)) in
-          CPatDelimiters (loc,"nat_scope",n)
+          CPatDelimiters (loc,"N",n)
       | "("; p = compound_pattern; ")" -> p
       | n = INT -> CPatNumeral (loc,Bignat.POS (Bignat.of_string n))
       | "-"; n = INT -> CPatNumeral (loc,Bignat.NEG (Bignat.of_string n))
+      | "`"; G_constr.test_ident_colon; key = string; ":"; c = pattern; "`" -> 
+          CPatDelimiters (loc,key,c)
     ] ]
   ;
   compound_pattern:
diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4
index 6476cec513..c298b0e3ff 100644
--- a/parsing/g_constr.ml4
+++ b/parsing/g_constr.ml4
@@ -65,6 +65,18 @@ let test_int_bang =
             end
         | _ -> raise Stream.Failure)
 
+(* Hack to parse "`id:...`" at level 0 without conflicting with
+   "`...`" from ZArith *)
+let test_ident_colon =
+  Gram.Entry.of_parser "test_int_bang"
+    (fun strm ->
+      match Stream.npeek 1 strm with
+        | [("IDENT", _)] ->
+            begin match Stream.npeek 2 strm with
+              | [_; ("", ":")] -> ()
+              | _ -> raise Stream.Failure
+            end
+        | _ -> raise Stream.Failure)
 
 GEXTEND Gram
   GLOBAL: constr9 lconstr constr sort global constr_pattern Constr.ident
@@ -95,7 +107,7 @@ GEXTEND Gram
   constr:
     [ "top" RIGHTA
       [ c1 = constr; "->"; c2 = constr -> CArrow (loc, c1, c2) ]
-    | "1"
+    | "1" RIGHTA
       [ "<"; p = lconstr; ">"; IDENT "Match"; c = constr; "with";
         cl = LIST0 constr; "end" ->
 	  COrderedCase (loc, MatchStyle, Some p, c, cl)
@@ -129,14 +141,14 @@ GEXTEND Gram
         IDENT "then"; c2 = constr; 
         IDENT "else"; c3 = constr LEVEL "top" ->
 	  COrderedCase (loc, IfStyle, Some p, c1, [c2; c3]) ]
-    | "0"
+    | "0" RIGHTA
       [ "?" -> CHole loc
       | "?"; n = Prim.natural -> CMeta (loc, n)
       | bll = binders; c = constr LEVEL "top" -> abstract_constr loc c bll
       (* Hack to parse syntax "(n)" as a natural number *)
       | "("; test_int_rparen; n = INT; ")" ->
 	  let n = CNumeral (loc,Bignat.POS (Bignat.of_string n)) in
-          CDelimiters (loc,"nat_scope",n)
+          CDelimiters (loc,"N",n)
       | "("; lc1 = lconstr; ":"; c = constr; (bl,body) = product_tail ->
           let id = coerce_to_name lc1 in
 	  CProdN (loc, ([id], c)::bl, body)
@@ -166,7 +178,9 @@ GEXTEND Gram
       | v = global -> CRef v
       | n = INT -> CNumeral (loc,Bignat.POS (Bignat.of_string n))
       | "-"; n = INT -> CNumeral (loc,Bignat.NEG (Bignat.of_string n))
-      | "!"; f = global -> CAppExpl (loc,f,[]) ] ]
+      | "!"; f = global -> CAppExpl (loc,f,[])
+      | "`"; test_ident_colon; key = string; ":"; c = constr; "`" -> 
+          CDelimiters (loc,key,c) ] ]
   ;
   lconstr:
     [ "10"
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 1d7519c99f..e94b513fb4 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -403,10 +403,11 @@ GEXTEND Gram
 	  Pp.warning "Class is obsolete"; VernacNop
 
 (* Implicit *)
+(*
       | IDENT "Syntactic"; "Definition"; id = base_ident; ":="; c = constr;
          n = OPT [ "|"; n = natural -> n ] ->
 	   VernacSyntacticDefinition (id,c,n)
-(*
+*)
       | IDENT "Syntactic"; "Definition"; id = IDENT; ":="; c = constr;
          n = OPT [ "|"; n = natural -> n ] ->
 	   let c = match n with
@@ -415,7 +416,6 @@ GEXTEND Gram
 		 CApp (loc,c,l)
 	     | None -> c in
 	   VernacNotation ("'"^id^"'",c,[],None)
-*)
       | IDENT "Implicits"; qid = global; "["; l = LIST0 natural; "]" ->
 	  VernacDeclareImplicits (qid,Some l)
       | IDENT "Implicits"; qid = global -> VernacDeclareImplicits (qid,None)
diff --git a/parsing/pcoq.ml4 b/parsing/pcoq.ml4
index fa0c3809e8..1a7df020c7 100644
--- a/parsing/pcoq.ml4
+++ b/parsing/pcoq.ml4
@@ -17,6 +17,7 @@ open Topconstr
 open Ast
 open Genarg
 open Tacexpr
+open Ppextend
 open Extend
 
 (* The lexer of Coq *)
@@ -492,16 +493,45 @@ let default_action_parser =
   Gram.Entry.of_parser "default_action_parser" 
     (fun strm -> Gram.Entry.parse_token (get_default_action_parser ()) strm)
 
-let entry_of_type allow_create = function
-  | ETConstr (_,Some 10) -> weaken_entry Constr.lconstr, None
-  | ETConstr (_,Some 9) -> weaken_entry Constr.constr9, None
-  | ETConstr (_,lev) -> weaken_entry Constr.constr, lev
+(* This determines if a reference to constr_n is a reference to the level
+   below wrt associativity (to be translated in camlp4 into "constr" without 
+   level) or to another level (to be translated into "constr LEVEL n") *)
+
+(* Camlp4 levels do not treat NonA *)
+let camlp4_assoc = function
+  | Some Gramext.NonA | None -> Gramext.LeftA
+  | Some a -> a
+
+(* Official Coq convention *)
+let coq_assoc = function
+  | None -> Gramext.LeftA
+  | Some a -> a
+
+let adjust_level assoc = function
+  (* If no associativity constraints, adopt the current one *)
+  | (n,BorderProd (_,Some Gramext.NonA)) -> None
+  (* Otherwise, deal with the current one *)
+  | (n,BorderProd (_,a)) when coq_assoc a = camlp4_assoc assoc -> None
+  | (n,BorderProd (left,a)) ->
+      let a = coq_assoc a in
+      if (left & a = Gramext.LeftA) or ((not left) & a = Gramext.RightA)
+      then Some n else Some (n-1)
+  | (8,InternalProd) -> None
+  | (n,InternalProd) -> Some n
+
+let compute_entry allow_create adjust = function
+  | ETConstr (10,_) -> weaken_entry Constr.lconstr, None
+  | ETConstr (9,_) -> weaken_entry Constr.constr9, None
+  | ETConstr (n,q) -> weaken_entry Constr.constr, adjust (n,q)
   | ETIdent -> weaken_entry Constr.ident, None
   | ETReference -> weaken_entry Constr.global, None
+  | ETPattern -> weaken_entry Constr.pattern, None
   | ETOther (u,n) ->
       let u = get_univ u in
       let e =
         try get_entry u n
         with e when allow_create -> create_entry u n ConstrArgType in
       object_of_typed_entry e, None
-  | ETPattern -> weaken_entry Constr.pattern, None
+
+let get_constr_entry = compute_entry true (fun (n,()) -> Some n)
+let get_constr_production_entry ass = compute_entry false (adjust_level ass)
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index d46a245ce7..467fe5f331 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -32,8 +32,11 @@ val type_of_typed_entry : typed_entry -> Extend.entry_type
 val object_of_typed_entry : typed_entry -> grammar_object Gram.Entry.e
 val weaken_entry : 'a Gram.Entry.e -> grammar_object Gram.Entry.e
 
-val entry_of_type :
-  bool -> constr_entry_type -> grammar_object Gram.Entry.e * int option
+val get_constr_entry :
+  constr_entry -> grammar_object Gram.Entry.e * int option
+
+val get_constr_production_entry : Gramext.g_assoc option -> 
+  constr_production_entry -> grammar_object Gram.Entry.e * int option
 
 val grammar_extend :
   'a Gram.Entry.e -> Gramext.position option ->
diff --git a/parsing/ppconstr.ml b/parsing/ppconstr.ml
index e49f531f16..e177bb6211 100644
--- a/parsing/ppconstr.ml
+++ b/parsing/ppconstr.ml
@@ -103,11 +103,8 @@ let pr_notation pr s env =
   let unpl, level = find_notation_printing_rule s in
   prlist (print_hunk pr env) unpl, level
 
-let pr_delimiters sc strm =
-  match find_delimiters sc with
-  | None -> anomaly "Delimiters without concrete syntax"
-  | Some (left,right) ->
-  assert (left <> "" && right <> "");
+let pr_delimiters key strm =
+  let left = "`"^key^":" and right = "`" in
   let lspace =
     if is_letter (left.[String.length left -1]) then str " " else mt () in
   let rspace =
diff --git a/parsing/prettyp.ml b/parsing/prettyp.ml
index d963d8644c..efcb5c8afa 100644
--- a/parsing/prettyp.ml
+++ b/parsing/prettyp.ml
@@ -298,13 +298,16 @@ let print_inductive sp = (print_mutual sp)
 let print_syntactic_def sep kn =
   let l = label kn in
   let c = Syntax_def.search_syntactic_definition dummy_loc kn in 
-  (str" Syntactic Definition " ++ pr_lab l ++ str sep ++ pr_rawterm c ++ fnl ())
+  (str" Syntactic Definition " ++ pr_lab l ++ str sep ++ 
+  Constrextern.without_symbols pr_rawterm c ++ fnl ())
+
 (*let print_module with_values kn = 
   str "Module " ++ pr_id (id_of_label (label kn)) ++ fnl () ++ fnl ()
 
 let print_modtype kn =
   str "Module Type " ++ pr_id (id_of_label (label kn)) ++ fnl () ++ fnl ()
 *)
+
 let print_leaf_entry with_values sep ((sp,kn as oname),lobj) =
   let tag = object_tag lobj in
   match (oname,tag) with
diff --git a/toplevel/command.ml b/toplevel/command.ml
index eb911b4d21..80c78c0860 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -119,8 +119,7 @@ let declare_definition ident local bl red_option c typopt =
         declare_global_definition ident ce' local
 
 let syntax_definition ident c =
-  let c = 
-interp_aconstr c in 
+  let c = interp_aconstr c in 
   Syntax_def.declare_syntactic_definition ident c;
   if_verbose message ((string_of_id ident) ^ " is now a syntax macro")
 
diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml
index 29324cb5fa..a3f0dcc2a2 100644
--- a/toplevel/metasyntax.ml
+++ b/toplevel/metasyntax.ml
@@ -76,14 +76,13 @@ allowed in abbreviatable expressions"
   let a = aux a in
   let find_type x =
     if List.mem x !bound_binders then (x,ETIdent) else
-    if List.mem x !bound_vars then (x,ETConstr ((10,E),None)) else
+    if List.mem x !bound_vars then (x,ETConstr (10,())) else
       error ((string_of_id x)^" is unbound in the right-hand-side") in
   let typs = List.map find_type vars in
   (a, typs)
 
 let _ = set_ast_to_rawconstr
-  (fun etyps a ->
-    let vl = List.map fst etyps in 
+  (fun vl a ->
     let r =
       for_grammar (interp_rawconstr_gen Evd.empty (Global.env()) [] false vl) a
     in
@@ -188,7 +187,7 @@ let add_tactic_grammar g =
 let print_grammar univ entry =
   let u = get_univ univ in
   let typ = explicitize_entry (fst u) entry in
-  let te,_ = entry_of_type false typ in
+  let te,_ = get_constr_entry typ in
   Gram.Entry.print te
 
 (* Infix, distfix, notations *)
@@ -234,22 +233,16 @@ type symbol =
 let prec_assoc = function
   | Some(Gramext.RightA) -> (L,E)
   | Some(Gramext.LeftA) -> (E,L)
+(*
   | Some(Gramext.NonA) -> (L,L)
   | None -> (L,L)   (* NONA by default *)
+*)
+  (* Camlp4 levels do not treat NonA *)
+  | Some(Gramext.NonA) -> (E,L)
+  | None -> (E,L)   (* NONA by default *)
 
 let level_rule (n,p) = if p = E then n else max (n-1) 0
 
-(* Find the digit code of the main entry of a sub-level and its associativity
-   (i.e. [9] means "constr9", [10] means "lconstr", [11] means "pattern",
-   otherwise "constr") *)
-
-let constr_rule = function
-  | (9|10 as n,E) -> Some n
-  | (9,L) -> None
-  | (10,L) -> Some 9
-  | (11,E) -> Some 11
-  | _ -> None
-
 (* For old ast printer *)
 let meta_pattern m = Pmeta(m,Tany)
 
@@ -262,7 +255,9 @@ let add_break l = function
   | _ -> l
 
 let precedence_of_entry_type = function
-  | ETConstr (prec,_) -> prec
+  | ETConstr (n,BorderProd (left,a)) ->
+      (n, let (lp,rp) = prec_assoc a in if left then lp else rp)
+  | ETConstr (n,InternalProd) -> (n,E)
   | _ -> 0,E
 
 (* For old ast printer *)
@@ -325,9 +320,7 @@ let string_of_symbol = function
   | Terminal s -> [s]
   | Break _ -> []
 
-let assoc_of_type = function
-  | (_,ETConstr (lp,_)) -> level_rule lp
-  | _ -> 0
+let assoc_of_type (_,typ) = level_rule (precedence_of_entry_type typ)
 
 let string_of_assoc = function
   | Some(Gramext.RightA) -> "RIGHTA"
@@ -366,14 +359,15 @@ let quote x =
 
 let is_symbol = function String s -> not (is_letter s.[0]) | _ -> false
 
-let rec find_symbols c_first c_last vars = function
+let rec find_symbols c_current c_next c_last vars = function
   | []    -> (vars, [])
   | String x :: sl when is_letter x.[0] ->
       let id = Names.id_of_string x in
       if List.mem_assoc id vars then
 	error ("Variable "^x^" occurs more than once");
-      let prec = if List.exists is_symbol sl then c_first else c_last in
-      let (vars,l) = find_symbols None c_last vars sl in
+(*      let prec = if List.exists is_symbol sl then c_current else c_last in*)
+      let prec = if sl <> [] then c_current else c_last in
+      let (vars,l) = find_symbols c_next c_next c_last vars sl in
       ((id,prec)::vars, NonTerminal id :: l)
 (*
   | "_"::sl ->
@@ -385,10 +379,10 @@ let rec find_symbols c_first c_last vars = function
       (vars, NonTerminal (prec, meta) :: l)
 *)
   | String s :: sl ->
-      let (vars,l) = find_symbols None c_last vars sl in
+      let (vars,l) = find_symbols c_next c_next c_last vars sl in
       (vars, Terminal (strip s) :: l)
   | WhiteSpace n :: sl ->
-      let (vars,l) = find_symbols c_first c_last vars sl in
+      let (vars,l) = find_symbols c_current c_next c_last vars sl in
       (vars, Break n :: l)
 
 let make_grammar_rule n assoc typs symbols ntn =
@@ -463,7 +457,7 @@ let interp_syntax_modifiers =
 	if List.mem_assoc id etyps then
 	  error (s^" is already assigned to an entry or constr level")
 	else
-	  let typ = ETConstr ((n,E), Some n) in
+	  let typ = ETConstr (n,()) in
 	  interp assoc level ((id,typ)::etyps) (SetItemLevel (idl,n)::l)
     | SetLevel n :: l ->
 	if level <> None then error "A level is mentioned more than twice"
@@ -483,20 +477,21 @@ let rec merge_entry_types etyps' = function
       e :: merge_entry_types (List.remove_assoc x etyps') etyps
 
 let set_entry_type etyps (x,typ) =
-  let typ = match typ with
-  | None -> 
-      (try List.assoc x etyps
-      with Not_found -> ETConstr ((10,E), Some 10))
-  | Some typ ->
-      let typ = ETConstr (typ,constr_rule typ) in
-      try List.assoc x etyps
-      with Not_found -> typ in
-  (x,typ)
+  let typ = try 
+    match List.assoc x etyps, typ with
+      | ETConstr (n,()), (_,BorderProd (left,_)) ->
+          ETConstr (n,BorderProd (left,None))
+      | ETConstr (n,()), (_,InternalProd) -> ETConstr (n,InternalProd)
+      | (ETPattern | ETIdent | ETOther _ | ETReference as t), _ -> t
+    with Not_found -> ETConstr typ
+  in (x,typ)
 
 let add_syntax_extension df modifiers =
   let (assoc,n,etyps,onlyparse) = interp_syntax_modifiers modifiers in
-  let (lp,rp) = prec_assoc assoc in
-  let (typs,symbs) = find_symbols (Some (n,lp)) (Some (n,rp)) [] (split df) in
+  let (typs,symbs) =
+    find_symbols
+      (n,BorderProd(true,assoc)) (10,InternalProd) (n,BorderProd(false,assoc))
+      [] (split df) in
   let typs = List.map (set_entry_type etyps) typs in
   let (prec,notation) = make_symbolic assoc n symbs typs in
   let gram_rule = make_grammar_rule n assoc typs symbs notation in
@@ -520,7 +515,9 @@ let open_notation i (_,(oldse,prec,ntn,scope,metas,pat,onlyparse,df)) =
       Esyntax.add_ppobject {sc_univ="constr";sc_entries=out_some oldse};
     (* Declare the interpretation *)
     if not b then
-      Symbols.declare_notation ntn scope (metas,pat) prec df onlyparse;
+      Symbols.declare_notation_interpretation ntn scope (metas,pat) prec df;
+    if not b & not onlyparse then
+      Symbols.declare_uninterpretation (NotationRule (ntn,scope)) (metas,pat)
   end
 
 let cache_notation o =
@@ -563,20 +560,13 @@ let make_old_pp_rule n symbols typs r ntn scope vars =
   let rule_name = ntn^"_"^scope^"_notation" in
   make_syntax_rule n rule_name symbols typs ast ntn scope
 
-let add_notation df a modifiers sc =
-  let toks = split df in
-  let (assoc,n,etyps,onlyparse) =
-    if modifiers = [] &
-      match toks with [String x] when quote(strip x) = x -> true | _ -> false
-    then
-      (* Means a Syntactic Definition *)
-      (None,0,[],false)
-    else
-      interp_syntax_modifiers modifiers
-  in
+let add_notation_in_scope df a modifiers sc toks =
+  let (assoc,n,etyps,onlyparse) = interp_syntax_modifiers modifiers in
   let scope = match sc with None -> Symbols.default_scope | Some sc -> sc in
-  let (lp,rp) = prec_assoc assoc in
-  let (typs,symbols) = find_symbols (Some (n,lp)) (Some (n,rp)) [] toks in
+  let (typs,symbols) =
+    find_symbols
+      (n,BorderProd(true,assoc)) (10,InternalProd) (n,BorderProd(false,assoc))
+      [] toks in
   let vars = List.map fst typs in
   (* To globalize... *)
   let r = interp_rawconstr_gen Evd.empty (Global.env()) [] false vars a in
@@ -599,6 +589,16 @@ let add_notation df a modifiers sc =
   Lib.add_anonymous_leaf
     (inNotation(old_pp_rule,prec,notation,scope,vars,a,onlyparse,df))
 
+let add_notation df a modifiers sc =
+  let toks = split df in
+  match toks with 
+    | [String x] when quote(strip x) = x & modifiers = [] ->
+        (* Means a Syntactic Definition *)
+        let ident = id_of_string (strip x) in
+        Syntax_def.declare_syntactic_definition ident (interp_aconstr a)
+    | _ ->
+        add_notation_in_scope df a modifiers sc toks
+
 (* TODO add boxes information in the expression *)
 
 let inject_var x = CRef (Ident (dummy_loc, id_of_string x))
@@ -640,16 +640,11 @@ let add_infix assoc n inf pr sc =
   add_notation ("x "^(quote inf)^" y") a (SetLevel n :: assoc) sc
 
 (* Delimiters *)
-let load_delimiters _ (_,(_,_,scope,dlm)) =
+let load_delimiters _ (_,(scope,dlm)) =
   Symbols.declare_scope scope
 
-let open_delimiters i (_,(gram_rule,pat_gram_rule,scope,dlm)) =
-  if i=1 then begin
-    (* For parsing *)
-    Egrammar.extend_grammar (Egrammar.Delimiters (scope,gram_rule,pat_gram_rule));
-    (* For printing *)
-    Symbols.declare_delimiters scope dlm
-  end
+let open_delimiters i (_,(scope,dlm)) =
+  if i=1 then Symbols.declare_delimiters scope dlm
 
 let cache_delimiters o =
   load_delimiters 1 o;
@@ -662,13 +657,5 @@ let (inDelim,outDelim) =
       load_function = load_delimiters;
       export_function = (fun x -> Some x) }
 
-let make_delimiter_rule key typ =
-  let e = Nameops.make_ident "e" None in
-  let symbols = [Terminal ("'"^key^":"); NonTerminal e; Terminal "'"] in
-  make_production [e,typ] symbols
-
 let add_delimiters scope key =
-  let gram_rule = make_delimiter_rule key (ETConstr ((0,E),Some 0)) in
-  let pat_gram_rule = make_delimiter_rule key ETPattern in
-  let dlms = ("'"^key^":", "'") in
-  Lib.add_anonymous_leaf (inDelim(gram_rule,pat_gram_rule,scope,dlms))
+  Lib.add_anonymous_leaf (inDelim(scope,key))