Utilisation des niveaux de camlp4 pour gérer les niveaux de constr; améliorations diverses de l'affichage; affinement de la syntaxe et des options de Notation; branchement de Syntactic Definition sur Notation

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

15 files changed, 325 insertions, 277 deletions

diff --git a/parsing/ast.ml b/parsing/ast.ml
index ae677979f..13989bcbb 100755
--- a/parsing/ast.ml
+++ b/parsing/ast.ml
@@ -345,6 +345,8 @@ let rec amatch alp sigma spat ast =
     | (Pmeta(pv,Tlist),_) -> grammar_type_error (loc ast,"Ast.amatch")
     | (Pmeta_slam(pv,pb), Slam(loc, Some s, b)) ->
         amatch alp (bind_env_ast sigma pv (Nvar(loc,s))) pb b
+    | (Pmeta_slam(pv,pb), Slam(loc, None, b)) ->
+        amatch alp (bind_env_ast sigma pv (Nvar(loc,id_of_string "_"))) pb b
     | (Pmeta_slam(pv,pb), Smetalam(loc, s, b)) ->
 	anomaly "amatch: match a pattern with an open ast"
     | (Pnode(nodp,argp), Node(loc,op,args)) when nodp = op ->
diff --git a/parsing/egrammar.ml b/parsing/egrammar.ml
index 33ca1214f..5b5777492 100644
--- a/parsing/egrammar.ml
+++ b/parsing/egrammar.ml
@@ -20,7 +20,7 @@ open Libnames
 (* State of the grammar extensions *)
 
 type all_grammar_command =
-  | Notation of (string * notation * prod_item list)
+  | Notation of (int * Gramext.g_assoc option * notation * prod_item list)
   | Delimiters of (scope_name * prod_item list * prod_item list)
   | Grammar of grammar_command
   | TacticGrammar of
@@ -35,6 +35,35 @@ let subst_all_grammar_command subst = function
 
 let (grammar_state : all_grammar_command list ref) = ref []
 
+
+(**************************************************************************)
+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;1;0]
+
+exception Found
+
+let find_position n =
+  let after = ref 8 in
+  let rec add_level q = function
+    | p::l when p > n -> p :: add_level p l
+    | p::l when p = n -> raise Found
+    | l -> after := q; n::l
+  in
+  try
+    numeric_levels := add_level 8 !numeric_levels;
+    Gramext.After (constr_level !after)
+  with
+      Found -> Gramext.Level (constr_level n)
+
 (* Interpretation of the right hand side of grammar rules *)
 
 (* When reporting errors, we add the name of the grammar rule that failed *)
@@ -78,13 +107,15 @@ 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) :: tl -> (* non-terminal *)
+    | Some (p, (ETConstr _| ETOther _)) :: tl -> (* 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)
     | Some (p, ETIdent) :: tl -> (* non-terminal *)
         Gramext.action (fun (v:identifier) ->
-	  make ((p,CRef (Ident (dummy_loc,v))) :: env) tl) in
+	  make ((p,CRef (Ident (dummy_loc,v))) :: env) tl)
+    | Some (p, ETPattern) :: tl -> 
+	failwith "Unexpected entry of type cases pattern" in
   make [] (List.rev pil)
 
 let make_cases_pattern_act f pil =
@@ -93,12 +124,12 @@ let make_cases_pattern_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) :: tl -> (* non-terminal *)
+    | Some (p, ETPattern) :: tl -> (* non-terminal *)
         Gramext.action (fun v -> make ((p,v) :: env) tl)
     | Some (p, ETReference) :: tl -> (* non-terminal *)
         Gramext.action (fun v -> make ((p,CPatAtom (dummy_loc,Some v)) :: env) tl)
-    | Some (p, ETIdent) :: tl ->
-	error "ident entry not admitted in patterns cases syntax extensions" in
+    | Some (p, (ETIdent | ETConstr _ | ETOther _)) :: tl ->
+	error "ident and constr entry not admitted in patterns cases syntax extensions" in
   make [] (List.rev pil)
 
 (* Grammar extension command. Rules are assumed correct.
@@ -108,17 +139,16 @@ let make_cases_pattern_act f pil =
  * annotations are added when type-checking the command, function
  * Extend.of_ast) *)
 
-let get_entry_type (u,n) =
-  if u = "constr" & n = "pattern" then Gram.Entry.obj Constr.pattern
-  else Gram.Entry.obj (object_of_typed_entry (get_entry (get_univ u) n))
-
 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)
-  | ProdPrimitive nt -> 
-      let eobj = get_entry_type nt in
-      Gramext.Snterm eobj
+  | 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)
 
 let symbol_of_prod_item univ = function
   | Term tok -> (Gramext.Stoken tok, None)
@@ -126,14 +156,6 @@ let symbol_of_prod_item univ = function
       let eobj = build_prod_item univ nt in
       (eobj, ovar)
 
-(*
-let make_rule univ etyp rule =
-  let pil = List.map (symbol_of_prod_item univ) rule.gr_production in
-  let (symbs,ntl) = List.split pil in
-  let act = make_act (rule.gr_name,etyp) rule.gr_action ntl in
-  (symbs, act)
-*)
-
 let make_rule univ etyp rule =
   let pil = List.map (symbol_of_prod_item univ) rule.gr_production in
   let (symbs,ntl) = List.split pil in
@@ -147,18 +169,19 @@ let make_rule univ etyp rule =
   let act = 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, ass, rls) =
+let extend_entry univ (te, etyp, pos, name, ass, rls) =
   let rules = List.rev (List.map (make_rule univ etyp) rls) in
-  grammar_extend (object_of_typed_entry te) None [(None, ass, rules)]
+  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; ge_type=typ; gl_assoc=ass; gl_rules=rls} =
-  let typ = entry_type_of_constr_entry_type typ in
-  let e = force_entry_type univ n typ in
-  (e,typ,ass,rls)
+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 pos = option_app find_position lev in
+  let name = option_app constr_level lev in
+  (e,typ,pos,name,ass,rls)
 
 (* Add a bunch of grammar rules. Does not check if it is well formed *)
 let extend_grammar_rules gram =
@@ -186,29 +209,31 @@ let make_gen_act f pil =
         Gramext.action (fun v -> make ((p,in_generic t v) :: env) tl) in
   make [] (List.rev pil)
 
-let extend_constr entry make_act pt =
+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 (symbs,ntl) = List.split pil in
   let act = make_act ntl in
-  grammar_extend entry None [(None, None, [symbs, act])]
+  grammar_extend entry pos [(level, assoc, [symbs, act])]
 
 let constr_entry name =
   object_of_typed_entry (get_entry (get_univ "constr") name)
 
-let extend_constr_notation (name,ntn,rule) =
+let extend_constr_notation (n,assoc,ntn,rule) =
   let mkact loc env = CNotation (loc,ntn,env) in
-  extend_constr (constr_entry name) (make_act mkact) rule
-
-let extend_constr_grammar (name,c,rule) =
-  let mkact loc env = CGrammar (loc,c,env) in
-  extend_constr (constr_entry name) (make_act mkact) rule
+  let (e,level) = entry_of_type false (ETConstr ((n,Ppextend.E),Some n)) in
+  let pos = option_app find_position level in
+  extend_constr e pos (option_app constr_level level,assoc) 
+    (make_act mkact) rule
 
 let extend_constr_delimiters (sc,rule,pat_rule) =
   let mkact loc env = CDelimiters (loc,sc,snd (List.hd env)) in
-  extend_constr (constr_entry "constr8") (make_act mkact) rule;
+  extend_constr (constr_entry "constr") (Some (Gramext.Level "top"))
+    (None,None)
+    (make_act mkact) rule;
   let mkact loc env = CPatDelimiters (loc,sc,snd (List.hd env)) in
-  extend_constr Constr.pattern (make_cases_pattern_act mkact) pat_rule
+  extend_constr Constr.pattern None (None,None)
+    (make_cases_pattern_act mkact) pat_rule
 
 (* These grammars are not a removable *)
 let make_rule univ f g (s,pt) =
@@ -246,7 +271,7 @@ let rec interp_entry_name u s =
     let e = get_entry (get_univ u) n in
     let o = object_of_typed_entry e in
     let t = type_of_typed_entry e in
-    t, Gramext.Snterm (Pcoq.Gram.Entry.obj o)
+    t,Gramext.Snterm (Pcoq.Gram.Entry.obj o)
 
 let qualified_nterm current_univ = function
   | NtQual (univ, en) -> (rename_command univ, rename_command en)
diff --git a/parsing/egrammar.mli b/parsing/egrammar.mli
index ff3f6284b..d24264abc 100644
--- a/parsing/egrammar.mli
+++ b/parsing/egrammar.mli
@@ -24,15 +24,13 @@ val unfreeze : frozen_t -> unit
 val init : unit -> unit
 
 type all_grammar_command =
-  | Notation of (string * notation * prod_item list)
+  | Notation of (int * Gramext.g_assoc option * notation * prod_item list)
   | Delimiters of (scope_name * prod_item list * prod_item list)
   | Grammar of grammar_command
   | TacticGrammar of (string * (string * grammar_production list) * Tacexpr.raw_tactic_expr) list
 
 val extend_grammar : all_grammar_command -> unit
 
-val extend_constr_grammar : string * aconstr * prod_item list -> unit
-
 (* Add grammar rules for tactics *)
 type grammar_tactic_production =
   | TacTerm of string
diff --git a/parsing/esyntax.ml b/parsing/esyntax.ml
index 76f4b3f19..859b5548a 100644
--- a/parsing/esyntax.ml
+++ b/parsing/esyntax.ml
@@ -186,7 +186,8 @@ let pr_parenthesis inherited se strm =
     
 let print_delimiters inh se strm = function
   | None -> pr_parenthesis inh se strm
-  | Some (left,right) ->
+  | Some sc ->
+      let (left,right) = out_some (find_delimiters sc) in
       assert (left <> "" && right <> "");
       let lspace =
 	if is_letter (left.[String.length left -1]) then str " " else mt () in
@@ -227,21 +228,21 @@ let call_primitive_parser rec_pr otherwise inherited scopes (se,env) =
 	  (* Test for a primitive printer; may raise Not_found *)
 	  let sc,pr = lookup_primitive_printer c in
 	  (* Look if scope [sc] associated to this printer is OK *)
-	  (match Symbols.find_numeral_printer sc scopes with
+	  (match Symbols.availability_of_numeral sc scopes with
 	    | None -> otherwise ()
-	    | Some (dlm,scopes) ->
+	    | Some scopt ->
 	        (* We can use this printer *)
 	        let node = Ast.pat_sub dummy_loc env e in
 	        match pr node with
-		  | Some strm -> print_delimiters inherited se strm dlm
+		  | Some strm -> print_delimiters inherited se strm scopt
 		  | None -> otherwise ())
     | [UNP_SYMBOLIC (sc,pat,sub)] ->
-	(match Symbols.find_notation sc pat scopes with
+	(match Symbols.availability_of_notation (sc,pat) scopes with
 	  | None -> otherwise ()
-	  | Some (dlm,scopes) ->
+	  | Some scopt ->
 	      print_delimiters inherited se
-		(print_syntax_entry rec_pr scopes env 
-		  {se with syn_hunks = [sub]}) dlm)
+		(print_syntax_entry rec_pr (option_cons scopt scopes) env 
+		  {se with syn_hunks = [sub]}) scopt)
     | _ ->
 	pr_parenthesis inherited se (print_syntax_entry rec_pr scopes env se)
   )
diff --git a/parsing/extend.ml b/parsing/extend.ml
index 0e1f72536..2e4eea4b0 100644
--- a/parsing/extend.ml
+++ b/parsing/extend.ml
@@ -19,13 +19,17 @@ open Topconstr
 open Genarg
 
 type entry_type = argument_type
-type constr_entry_type = ETConstr | ETIdent | ETReference
+type constr_entry_type =
+  | ETIdent | ETReference
+  | ETConstr of (int * parenRelation) * int option
+  | ETPattern
+  | ETOther of string * string
 
 type nonterm_prod =
   | ProdList0 of nonterm_prod
   | ProdList1 of nonterm_prod
   | ProdOpt of nonterm_prod
-  | ProdPrimitive of (string * string)
+  | ProdPrimitive of constr_entry_type
 
 type prod_item =
   | Term of Token.pattern
@@ -38,7 +42,6 @@ type grammar_rule = {
 
 type grammar_entry = { 
   ge_name : string;
-  ge_type : constr_entry_type;
   gl_assoc : Gramext.g_assoc option;
   gl_rules : grammar_rule list }
 
@@ -56,18 +59,20 @@ type entry_context = (identifier * constr_entry_type) 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 vars = function
-  | SimpleAction (loc,ConstrNode a) -> !ast_to_rawconstr vars a
-  | SimpleAction (loc,CasesPatternNode a) -> failwith "TODO:act_of_ast: cases_pattern"
+let act_of_ast env = function
+  | SimpleAction (loc,ConstrNode a) -> !ast_to_rawconstr env a
+  | SimpleAction (loc,CasesPatternNode a) -> 
+      failwith "TODO:act_of_ast: cases_pattern"
   | CaseAction _ -> failwith "case/let not supported"
 
 let to_act_check_vars = act_of_ast
 
 type syntax_modifier =
-  | SetItemLevel of string * int
+  | SetItemLevel of string list * int
   | SetLevel of int
   | SetAssoc of Gramext.g_assoc
   | SetEntryType of string * constr_entry_type
+  | SetOnlyParsing
 
 type nonterm =
   | NtShort of string
@@ -76,8 +81,7 @@ type grammar_production =
   | VTerm of string
   | VNonTerm of loc * nonterm * Names.identifier option
 type raw_grammar_rule = string * grammar_production list * grammar_action
-type raw_grammar_entry = 
-  string * constr_entry_type * grammar_associativity * raw_grammar_rule list
+type raw_grammar_entry = string * grammar_associativity * raw_grammar_rule list
 
 let subst_grammar_rule subst gr =
   { gr with gr_action = subst_aconstr subst gr.gr_action }
@@ -141,55 +145,85 @@ let rename_command nt =
   else if nt = "lassoc_command4" then warn nt "lassoc_constr4"
   else nt
 
-let qualified_nterm current_univ = function
-  | NtQual (univ, en) -> (rename_command univ, rename_command en)
-  | NtShort en -> (current_univ, rename_command en)
-
-let entry_type_of_constr_entry_type = function
-  | ETConstr -> ConstrArgType
-  | ETIdent -> IdentArgType
-  | ETReference -> RefArgType
-
-let constr_entry_of_entry = function
-  | ConstrArgType -> ETConstr
-  | IdentArgType -> ETIdent
-  | RefArgType -> ETReference
-  | _ -> error "Cannot arbitrarily extend non constr/ident/ref entries"
-
-let nterm loc (get_entry_type,univ) nont =
-  let nt = qualified_nterm univ nont in
-  try (nt,constr_entry_of_entry (get_entry_type nt))
-  with Not_found -> 
-    let (s,n) = nt in
-    user_err_loc(loc,"Externd.nterm",str("unknown grammar entry: "^s^":"^n))
+(* This translates constr0, constr1, ... level into camlp4 levels of constr *)
+
+let explicitize_entry 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)
+  | "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
+  | NtQual (univ, en) ->
+      let univ = rename_command univ in
+      clever_explicitize_entry univ (rename_command en) from ass pos
+  | NtShort en ->
+      clever_explicitize_entry current_univ (rename_command en) from ass pos
+
+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
+  check_entry check_entry_type typ;
+  typ
 
 let prod_item univ env = function
   | VTerm s -> env, Term (terminal s)
   | VNonTerm (loc, nt, Some p) ->
-     let (nont, etyp) = nterm loc univ nt in
-      ((p, etyp) :: env, NonTerm (ProdPrimitive nont, Some (p,etyp)))
+     let typ = nterm loc univ nt in
+      ((p, typ) :: env, NonTerm (ProdPrimitive typ, Some (p,typ)))
   | VNonTerm (loc, nt, None) ->
-      let (nont, etyp) = nterm loc univ nt in 
-      env, NonTerm (ProdPrimitive nont, None)
+      let typ = nterm loc univ nt in 
+      env, NonTerm (ProdPrimitive typ, None)
 
-let rec prod_item_list univ penv pil =
+let rec prod_item_list univ penv pil start =
   match pil with
     | [] -> [], penv
     | pi :: pitl ->
-	let (env, pic) = prod_item univ penv pi in
-	let (pictl, act_env) = prod_item_list univ env pitl in
+	let pos = if pitl=[] then Some false else start in
+	let (env, pic) = prod_item (univ,pos) penv pi in
+	let (pictl, act_env) = prod_item_list univ env pitl None in
         (pic :: pictl, act_env)
 
-let gram_rule univ etyp (name,pil,act) =
-  let (pilc, act_env) = prod_item_list univ [] pil in
+let gram_rule univ (name,pil,act) =
+  let (pilc, act_env) = prod_item_list univ [] pil (Some true) in
   let a = to_act_check_vars act_env act in
   { gr_name = name; gr_production = pilc; gr_action = a }
 
-let gram_entry univ (nt, etyp, ass, rl) =
-  { ge_name = rename_command nt;
-    ge_type = etyp;
+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 etyp) rl }
+    gl_rules = List.map (gram_rule (univ,name,ass)) rl }
 
 let interp_grammar_command univ ge entryl =
   let univ = rename_command univ in
diff --git a/parsing/extend.mli b/parsing/extend.mli
index 13e3ee067..771434ea3 100644
--- a/parsing/extend.mli
+++ b/parsing/extend.mli
@@ -20,15 +20,17 @@ open Genarg
 (*i*)
 
 type entry_type = argument_type
-type constr_entry_type = ETConstr | ETIdent | ETReference
-
-val entry_type_of_constr_entry_type : constr_entry_type -> entry_type
+type constr_entry_type =
+  | ETIdent | ETReference
+  | ETConstr of (int * parenRelation) * int option
+  | ETPattern
+  | ETOther of string * string
 
 type nonterm_prod =
   | ProdList0 of nonterm_prod
   | ProdList1 of nonterm_prod
   | ProdOpt of nonterm_prod
-  | ProdPrimitive of (string * string)
+  | ProdPrimitive of constr_entry_type
 
 type prod_item =
   | Term of Token.pattern
@@ -41,7 +43,6 @@ type grammar_rule = {
 
 type grammar_entry = { 
   ge_name : string;
-  ge_type : constr_entry_type;
   gl_assoc : Gramext.g_assoc option;
   gl_rules : grammar_rule list }
 
@@ -57,10 +58,11 @@ val to_act_check_vars : entry_context -> grammar_action -> aconstr
 val set_ast_to_rawconstr : (entry_context -> constr_expr -> aconstr) -> unit
 
 type syntax_modifier =
-  | SetItemLevel of string * int
+  | SetItemLevel of string list * int
   | SetLevel of int
   | SetAssoc of Gramext.g_assoc
   | SetEntryType of string * constr_entry_type
+  | SetOnlyParsing
 
 type nonterm =
   | NtShort of string
@@ -69,13 +71,14 @@ type grammar_production =
   | VTerm of string
   | VNonTerm of loc * nonterm * Names.identifier option
 type raw_grammar_rule = string * grammar_production list * grammar_action
-type raw_grammar_entry = 
-  string * constr_entry_type * grammar_associativity * raw_grammar_rule list
+type raw_grammar_entry = string * grammar_associativity * raw_grammar_rule list
 
 val terminal : string -> string * string
 
 val rename_command : string -> string
 
+val explicitize_entry : string -> string -> constr_entry_type
+
 val subst_grammar_command : 
   Names.substitution -> grammar_command -> grammar_command
 
@@ -90,10 +93,6 @@ type 'pat unparsing_hunk =
   | UNP_TAB
   | UNP_FNL
   | UNP_SYMBOLIC of string * string * 'pat unparsing_hunk
-(*
-  | UNP_INFIX of Libnames.extended_global_reference * string * string *
-      (parenRelation * parenRelation)
-*)
 
 (*val subst_unparsing_hunk : 
   Names.substitution -> (Names.substitution -> 'pat -> 'pat) -> 
@@ -129,7 +128,7 @@ type syntax_rule = string * Coqast.t * Coqast.t unparsing_hunk list
 type raw_syntax_entry = precedence * syntax_rule list
 
 val interp_grammar_command :
-  string -> (string * string -> Genarg.argument_type) -> 
+  string -> (string * string -> unit) -> 
       raw_grammar_entry list -> grammar_command
 
 val interp_syntax_entry :
diff --git a/parsing/g_basevernac.ml4 b/parsing/g_basevernac.ml4
index 77f587894..55a350447 100644
--- a/parsing/g_basevernac.ml4
+++ b/parsing/g_basevernac.ml4
@@ -153,7 +153,8 @@ GEXTEND Gram
 	  VernacRemoveOption (PrimaryTable table, v) ] ]
   ;
   printable:
-    [ [ IDENT "All" -> PrintFullContext
+    [ [ IDENT "Term"; qid = global -> PrintName qid
+      | IDENT "All" -> PrintFullContext
       | IDENT "Section"; s = global -> PrintSectionContext s
       | "Grammar"; uni = IDENT; ent = IDENT ->
           (* This should be in "syntax" section but is here for factorization*)
@@ -173,7 +174,8 @@ GEXTEND Gram
       | IDENT "Hint" -> PrintHintGoal
       | IDENT "Hint"; qid = global -> PrintHint qid
       | IDENT "Hint"; "*" -> PrintHintDb
-      | IDENT "HintDb"; s = IDENT  -> PrintHintDbName s ] ]
+      | IDENT "HintDb"; s = IDENT -> PrintHintDbName s
+      | IDENT "Scope"; s = IDENT -> PrintScope s ] ]
   ;
   option_value:
     [ [ n  = integer   -> IntValue n
@@ -217,14 +219,14 @@ GEXTEND Gram
      | "Syntax"; u = univ; el = LIST1 syntax_entry SEP ";" ->
          VernacSyntax (u,el)
 
-     | "Syntax"; IDENT "Extension"; s = STRING; 
+     | "Uninterpreted"; IDENT "Notation"; s = STRING; 
 	 l = [ "("; l = LIST1 syntax_modifier SEP ","; ")" -> l | -> [] ]
 	 -> VernacSyntaxExtension (s,l)
 
      | IDENT "Open"; IDENT "Scope"; sc = IDENT -> VernacOpenScope sc
 
-     | IDENT "Delimiters"; left = STRING; sc = IDENT; right = STRING ->
-	 VernacDelimiters (sc,(left,right))
+     | IDENT "Delimits"; IDENT "Scope"; sc = IDENT; "with"; key = IDENT ->
+	 VernacDelimiters (sc,("`"^key^":","`"))
 
      | IDENT "Arguments"; IDENT "Scope"; qid = global;
          "["; scl = LIST0 opt_scope; "]" -> VernacArgumentsScope (qid,scl)
@@ -233,23 +235,27 @@ GEXTEND Gram
 	 sc = OPT [ ":"; sc = IDENT -> sc ] -> VernacInfix (a,n,op,p,sc)
      | IDENT "Distfix"; a = entry_prec; n = natural; s = STRING; p = global;
 	 sc = OPT [ ":"; sc = IDENT -> sc ] -> VernacDistfix (a,n,s,p,sc)
-     | IDENT "Notation"; a = entry_prec; n = natural; s = STRING; c = constr;
+     | IDENT "Notation"; s = IDENT; ":="; c = constr ->
+	 VernacNotation ("'"^s^"'",c,[],None)
+     | IDENT "Notation"; s = STRING; ":="; c = constr;
          modl = [ "("; l = LIST1 syntax_modifier SEP ","; ")" -> l | -> [] ];
-	 sc = OPT [ ":"; sc = IDENT -> sc ] ->
-	   let a = match a with None -> Gramext.LeftA | Some a -> a in
-	   VernacNotation (s,c,(SetAssoc a)::(SetLevel n)::modl,sc)
+	 sc = OPT [ ":"; sc = IDENT -> sc ] -> VernacNotation (s,c,modl,sc)
 
      (* "Print" "Grammar" should be here but is in "command" entry in order 
         to factorize with other "Print"-based vernac entries *)
   ] ]
   ;
   syntax_modifier:
-    [ [ x = IDENT; IDENT "at"; IDENT "level"; n = natural -> SetItemLevel (x,n)
+    [ [ x = IDENT; IDENT "at"; IDENT "level"; n = natural -> 
+        SetItemLevel ([x],n)
+      | x = IDENT; ","; l = LIST1 IDENT SEP ","; IDENT "at"; IDENT "level";
+        n = natural -> SetItemLevel (x::l,n)
       | IDENT "at"; IDENT "level"; n = natural -> SetLevel n
       | IDENT "left"; IDENT "associativity" -> SetAssoc Gramext.LeftA
       | IDENT "right"; IDENT "associativity" -> SetAssoc Gramext.RightA
       | IDENT "no"; IDENT "associativity" -> SetAssoc Gramext.NonA
-      | x = IDENT; typ = syntax_extension_type -> SetEntryType (x,typ) ] ]
+      | x = IDENT; typ = syntax_extension_type -> SetEntryType (x,typ)
+      | IDENT "only"; IDENT "parsing" -> SetOnlyParsing ] ]
   ;
   syntax_extension_type:
     [ [ IDENT "ident" -> ETIdent | IDENT "global" -> ETReference ] ]
@@ -259,9 +265,9 @@ GEXTEND Gram
   ;
   (* Syntax entries for Grammar. Only grammar_entry is exported *)
   grammar_entry:
-    [[ nont = IDENT; etyp = set_entry_type; ":=";
+    [[ nont = IDENT; set_entry_type; ":=";
        ep = entry_prec; OPT "|"; rl = LIST0 grammar_rule SEP "|" ->
-	 (nont,etyp,ep,rl) ]]
+	 (nont,ep,rl) ]]
   ;
   entry_prec:
     [[ IDENT "LEFTA" -> Some Gramext.LeftA
@@ -366,13 +372,8 @@ GEXTEND Gram
      | [ ":"; IDENT "ast" -> () | -> () ] -> Ast.ETast ]]
   ;
   set_entry_type:
-    [[ ":"; et = entry_type -> set_default_action_parser et;
-       let a = match et with
-	 | ConstrParser -> ETConstr
-	 | CasesPatternParser ->
-	     failwith "entry_type_of_parser: cases_pattern, TODO" in
-       a
-     | -> ETConstr ]]
+    [[ ":"; et = entry_type -> set_default_action_parser et
+     | -> () ]]
   ;
   entry_type:
     [[ IDENT "ast"; IDENT "list" -> Util.error "type ast list no longer supported"
diff --git a/parsing/g_cases.ml4 b/parsing/g_cases.ml4
index 1b8be4f4f..a7b27de23 100644
--- a/parsing/g_cases.ml4
+++ b/parsing/g_cases.ml4
@@ -20,7 +20,7 @@ let pair loc =
   Qualid (loc, Libnames.qualid_of_string "Coq.Init.Datatypes.pair")
 
 GEXTEND Gram
-  GLOBAL: constr1 pattern;
+  GLOBAL: constr pattern;
 
   pattern:
     [ [ r = Prim.reference -> CPatAtom (loc,Some r)
@@ -52,8 +52,7 @@ GEXTEND Gram
   ne_eqn_list:
     [ [ leqn = LIST1 equation SEP "|" -> leqn ] ]
   ;
-
-  constr1:
+  constr: LEVEL "1"
     [ [ "<"; p = lconstr; ">"; "Cases"; lc = LIST1 constr; "of";
         OPT "|"; eqs = ne_eqn_list; "end" ->
 	  CCases (loc, Some p, lc, eqs)
diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4
index 8644cb724..6476cec51 100644
--- a/parsing/g_constr.ml4
+++ b/parsing/g_constr.ml4
@@ -52,12 +52,23 @@ let test_int_rparen =
             end
         | _ -> raise Stream.Failure)
 
+(* Hack to parse "n" at level 0 without conflicting with "n!" at level 91 *)
+(* admissible notation "(n)" *)
+let test_int_bang =
+  Gram.Entry.of_parser "test_int_bang"
+    (fun strm ->
+      match Stream.npeek 1 strm with
+        | [("INT", n)] ->
+            begin match Stream.npeek 2 strm with
+              | [_; ("", "!")] -> ()
+              | _ -> raise Stream.Failure
+            end
+        | _ -> raise Stream.Failure)
+
 
 GEXTEND Gram
-  GLOBAL: constr0 constr1 constr2 constr3 lassoc_constr4 constr5
-          constr6 constr7 constr8 constr9 constr10 lconstr constr
-          ne_name_comma_list ne_constr_list sort
-          global constr_pattern Constr.ident;
+  GLOBAL: constr9 lconstr constr sort global constr_pattern Constr.ident
+          (*ne_name_comma_list*);
   Constr.ident:
     [ [ id = Prim.ident -> id
 
@@ -70,12 +81,6 @@ GEXTEND Gram
       (* This is used in quotations *)
       | id = METAIDENT -> Ident (loc,id_of_string id) ] ]
   ;
-  constr:
-    [ [ c = constr8 -> c ] ]
-  ;
-  lconstr:
-    [ [ c = constr10 -> c ] ]
-  ;
   constr_pattern:
     [ [ c = constr -> c ] ]
   ;
@@ -87,10 +92,47 @@ GEXTEND Gram
       | "Prop" -> RProp Null
       | "Type" -> RType None ] ]
   ;
-  constr0:
-    [ [ "?" -> CHole loc
+  constr:
+    [ "top" RIGHTA
+      [ c1 = constr; "->"; c2 = constr -> CArrow (loc, c1, c2) ]
+    | "1"
+      [ "<"; p = lconstr; ">"; IDENT "Match"; c = constr; "with";
+        cl = LIST0 constr; "end" ->
+	  COrderedCase (loc, MatchStyle, Some p, c, cl)
+      | "<"; p = lconstr; ">"; IDENT "Case"; c = constr; "of";
+        cl = LIST0 constr; "end" ->
+	  COrderedCase (loc, RegularStyle, Some p, c, cl)
+      | IDENT "Case"; c = constr; "of"; cl = LIST0 constr; "end" ->
+          COrderedCase (loc, RegularStyle, None, c, cl)
+      | IDENT "Match"; c = constr; "with"; cl = LIST1 constr; "end" ->
+          COrderedCase (loc, MatchStyle, None, c, cl)
+      | IDENT "let"; "("; b = ne_name_comma_list; ")"; "=";
+        c = constr; "in"; c1 = constr LEVEL "top"->
+          (* TODO: right loc *)
+	  COrderedCase
+            (loc, LetStyle, None, c, [CLambdaN (loc, [b, CHole loc], c1)])
+      | IDENT "let"; na = name; "="; c = opt_casted_constr; 
+	"in"; c1 = constr LEVEL "top" ->
+          CLetIn (loc, na, c, c1)
+      | IDENT "if"; c1 = constr;
+        IDENT "then"; c2 = constr;
+        IDENT "else"; c3 = constr LEVEL "top" ->
+	  COrderedCase (loc, IfStyle, None, c1, [c2; c3])
+      | "<"; p = lconstr; ">";
+        IDENT "let"; "("; b = ne_name_comma_list; ")"; "="; c = constr; 
+        "in"; c1 = constr LEVEL "top" ->
+          (* TODO: right loc *)
+	  COrderedCase (loc, LetStyle, Some p, c,
+            [CLambdaN (loc, [b, CHole loc], c1)])
+      | "<"; p = lconstr; ">";
+        IDENT "if"; c1 = constr;
+        IDENT "then"; c2 = constr; 
+        IDENT "else"; c3 = constr LEVEL "top" ->
+	  COrderedCase (loc, IfStyle, Some p, c1, [c2; c3]) ]
+    | "0"
+      [ "?" -> CHole loc
       | "?"; n = Prim.natural -> CMeta (loc, n)
-      | bll = binders; c = constr -> abstract_constr loc c bll
+      | 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
@@ -99,7 +141,7 @@ GEXTEND Gram
           let id = coerce_to_name lc1 in
 	  CProdN (loc, ([id], c)::bl, body)
 (* TODO: Syntaxe (_:t...)t et (_,x...)t *)
-      | "("; lc1 = lconstr; ","; lc2 = lconstr; ":"; c = constr; 
+      | "("; lc1 = lconstr; ","; lc2 = lconstr; ":"; c = constr;
         (bl,body) = product_tail ->
           let id1 = coerce_to_name lc1 in
           let id2 = coerce_to_name lc2 in
@@ -124,70 +166,11 @@ 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,[])
-    ] ]
-  ;
-  constr1:
-    [ [ "<"; p = lconstr; ">"; IDENT "Match"; c = constr; "with";
-        cl = LIST0 constr; "end" ->
-	  COrderedCase (loc, MatchStyle, Some p, c, cl)
-      | "<"; p = lconstr; ">"; IDENT "Case"; c = constr; "of";
-        cl = LIST0 constr; "end" ->
-	  COrderedCase (loc, RegularStyle, Some p, c, cl)
-      | IDENT "Case"; c = constr; "of"; cl = LIST0 constr; "end" ->
-          COrderedCase (loc, RegularStyle, None, c, cl)
-      | IDENT "Match"; c = constr; "with"; cl = LIST1 constr; "end" ->
-          COrderedCase (loc, MatchStyle, None, c, cl)
-      | IDENT "let"; "("; b = ne_name_comma_list; ")"; "=";
-        c = constr; "in"; c1 = constr->
-          (* TODO: right loc *)
-	  COrderedCase
-            (loc, LetStyle, None, c, [CLambdaN (loc, [b, CHole loc], c1)])
-      | IDENT "let"; na = name; "="; c = opt_casted_constr; "in"; c1 = constr
-          -> CLetIn (loc, na, c, c1)
-      | IDENT "if"; c1 = constr; IDENT "then"; c2 = constr;
-        IDENT "else"; c3 = constr ->
-	  COrderedCase (loc, IfStyle, None, c1, [c2; c3])
-      | "<"; p = lconstr; ">";
-        IDENT "let"; "("; b = ne_name_comma_list; ")"; "=";
-        c = constr; "in"; c1 = constr ->
-          (* TODO: right loc *)
-	  COrderedCase (loc, LetStyle, Some p, c,
-            [CLambdaN (loc, [b, CHole loc], c1)])
-      | "<"; p = lconstr; ">";
-        IDENT "if"; c1 = constr; IDENT "then";
-        c2 = constr; IDENT "else"; c3 = constr ->
-	  COrderedCase (loc, IfStyle, Some p, c1, [c2; c3])
-      | c = constr0 -> c ] ]
-  ;
-  constr2: (* ~ will be here *)
-    [ [ c = constr1 -> c ] ]
+      | "!"; f = global -> CAppExpl (loc,f,[]) ] ]
   ;
-  constr3:
-    [ [ c1 = constr2 -> c1 ] ]
-  ;
-  lassoc_constr4:
-    [ [ c1 = constr3 -> c1 ] ]
-  ;
-  constr5:
-    [ [ c1 = lassoc_constr4 -> c1 ] ]
-  ;
-  constr6:  (* /\ will be here *)
-    [ [ c1 = constr5 -> c1 ] ]
-  ;
-  constr7:  (* \/ will be here *)
-    [ RIGHTA [ c1 = constr6 -> c1 ] ]
-  ;
-  constr8:  (* <-> will be here *)
-    [ [ c1 = constr7 -> c1
-      | c1 = constr7; "->"; c2 = constr8 -> CArrow (loc, c1, c2) ] ]
-  ;
-  constr9:
-    [ [ c1 = constr8 -> c1
-      | c1 = constr8; "::"; c2 = constr8 -> CCast (loc, c1, c2) ] ]
-  ;
-  constr10:
-    [ [ "!"; f = global; args = LIST0 constr9 -> CAppExpl (loc, f, args)
+  lconstr:
+    [ "10"
+      [ "!"; f = global; args = LIST0 constr9 -> CAppExpl (loc, f, args)
 (*
       | "!"; f = global; "with"; b = binding_list ->
 	  <:ast< (APPLISTWITH $f $b) >>
@@ -195,11 +178,19 @@ GEXTEND Gram
       | f = constr9; args = LIST1 constr91 -> CApp (loc, f, args)
       | f = constr9 -> f ] ]
   ;
+  constr91:
+    [ [ test_int_bang; n = INT; "!"; c = constr9 ->
+        (c, Some (int_of_string n))
+      | c = constr9 -> (c, None) ] ]
+  ;
+  constr9:
+    [ [ c1 = constr -> c1
+      | c1 = constr; "::"; c2 = constr -> CCast (loc, c1, c2) ] ]
+  ;
   ne_name_comma_list:
     [ [ nal = LIST1 name SEP "," -> nal ] ]
   ;
   name_comma_list_tail:
-
     [ [ ","; idl = ne_name_comma_list -> idl
       | -> [] ] ]
   ;
@@ -241,12 +232,6 @@ GEXTEND Gram
     [ [ ":"; c = constr -> c 
       | -> CHole loc ] ]
   ;
-  constr91:
-    [ [ n = natural; "!"; c = constr9 -> (c, Some n)
-      | n = natural ->
-          (CNumeral (loc, Bignat.POS (Bignat.of_string (string_of_int n))), None)
-      | c = constr9 -> (c, None) ] ]
-  ;
   fixbinder:
     [ [ id = base_ident; "/"; recarg = natural; ":"; type_ = constr;
         ":="; def = constr ->
diff --git a/parsing/g_proofs.ml4 b/parsing/g_proofs.ml4
index 52100764d..951e75815 100644
--- a/parsing/g_proofs.ml4
+++ b/parsing/g_proofs.ml4
@@ -108,7 +108,7 @@ GEXTEND Gram
       | IDENT "Immediate"; c = Constr.constr -> fun name -> HintsImmediate [Some name, c]
       | IDENT "Unfold"; qid = global -> fun name -> HintsUnfold [Some name,qid]
       | IDENT "Constructors"; c = global -> fun n -> HintsConstructors (n,c)
-      | IDENT "Extern"; n = natural; c = Constr.constr8 ; tac = tactic ->
+      | IDENT "Extern"; n = natural; c = Constr.constr ; tac = tactic ->
 	  fun name -> HintsExtern (name,n,c,tac) ] ]
   ;
   hints:
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 36619758a..7a8f82478 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -403,9 +403,19 @@ 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
+	     | Some n ->
+		 let l = list_tabulate (fun _ -> (CHole (loc),None)) n in
+		 CApp (loc,c,l)
+	     | None -> c in
+	   VernacNotation ("'"^id^"'",c,[],None)
 
       | IDENT "Implicits"; qid = global; "["; l = LIST0 natural; "]" ->
 	  VernacDeclareImplicits (qid,Some l)
diff --git a/parsing/pcoq.ml4 b/parsing/pcoq.ml4
index 6472dbaf5..fa0c3809e 100644
--- a/parsing/pcoq.ml4
+++ b/parsing/pcoq.ml4
@@ -69,6 +69,7 @@ type typed_entry = entry_type * grammar_object G.Entry.e
 let in_typed_entry t e = (t,Gramobj.weaken_entry e)
 let type_of_typed_entry (t,e) = t
 let object_of_typed_entry (t,e) = e
+let weaken_entry x = Gramobj.weaken_entry x
 
 module type Gramtypes =
 sig
@@ -169,21 +170,6 @@ let map_entry f en =
 let parse_string f x =
   let strm = Stream.of_string x in Gram.Entry.parse f (Gram.parsable strm)
 
-(*
-let entry_type ast =
-  match ast with
-    | Coqast.Id (_, "LIST") -> ETastl
-    | Coqast.Id (_, "AST") -> ETast
-    | _ -> invalid_arg "Ast.entry_type"
-*)
-
-(*
-let entry_type ast =
-  match ast with
-    | AstListType -> ETastl
-    | _ -> ETast
-*)
-
 type gram_universe = (string, typed_entry) Hashtbl.t
 
 let trace = ref false
@@ -353,27 +339,12 @@ module Constr =
 
     (* Entries that can be refered via the string -> Gram.Entry.e table *)
     let constr = gec_constr "constr"
-    let constr0 = gec_constr "constr0"
-    let constr1 = gec_constr "constr1"
-    let constr2 = gec_constr "constr2"
-    let constr3 = gec_constr "constr3"
-    let lassoc_constr4 = gec_constr "lassoc_constr4"
-    let constr5 = gec_constr "constr5"
-    let constr6 = gec_constr "constr6"
-    let constr7 = gec_constr "constr7"
-    let constr8 = gec_constr "constr8"
     let constr9 = gec_constr "constr9"
-    let constr91 = gec_constr "constr91"
-    let constr10 = gec_constr "constr10"
     let constr_eoi = eoi_entry constr
     let lconstr = gec_constr "lconstr"
-    let sort = make_gen_entry uconstr rawwit_sort "sort"
-
     let ident = make_gen_entry uconstr rawwit_ident "ident"
     let global = make_gen_entry uconstr rawwit_ref "global"
-
-    let ne_name_comma_list = Gram.Entry.create "constr:ne_name_comma_list"
-    let ne_constr_list = gec_constr_list "ne_constr_list"
+    let sort = make_gen_entry uconstr rawwit_sort "sort"
     let pattern = Gram.Entry.create "constr:pattern"
     let constr_pattern = gec_constr "constr_pattern"
   end
@@ -520,3 +491,17 @@ let set_default_action_parser = function
 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
+  | ETIdent -> weaken_entry Constr.ident, None
+  | ETReference -> weaken_entry Constr.global, 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
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index a0f5a55c0..d46a245ce 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -30,6 +30,10 @@ type typed_entry
 
 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 grammar_extend :
   'a Gram.Entry.e -> Gramext.position option ->
@@ -56,6 +60,7 @@ val get_univ : string -> string * gram_universe
 val get_entry : string * gram_universe -> string -> typed_entry
 
 val entry_type : string * gram_universe -> string -> entry_type option
+
 val get_entry_type : string * string -> entry_type
 val create_entry_if_new :
   string * gram_universe -> string -> entry_type -> unit
@@ -118,30 +123,14 @@ module Prim :
 module Constr :
   sig
     val constr : constr_expr Gram.Entry.e
-    val constr0 : constr_expr Gram.Entry.e
-    val constr1 : constr_expr Gram.Entry.e
-    val constr2 : constr_expr Gram.Entry.e
-    val constr3 : constr_expr Gram.Entry.e
-    val lassoc_constr4 : constr_expr Gram.Entry.e
-    val constr5 : constr_expr Gram.Entry.e
-    val constr6 : constr_expr Gram.Entry.e
-    val constr7 : constr_expr Gram.Entry.e
-    val constr8 : constr_expr Gram.Entry.e
     val constr9 : constr_expr Gram.Entry.e
-    val constr91 : constr_expr Gram.Entry.e
-    val constr10 : constr_expr Gram.Entry.e
     val constr_eoi : constr_expr Gram.Entry.e
     val lconstr : constr_expr Gram.Entry.e
     val ident : identifier Gram.Entry.e
     val global : reference Gram.Entry.e
-    val ne_name_comma_list : name located list Gram.Entry.e
-    val ne_constr_list : constr_expr list Gram.Entry.e
     val sort : rawsort Gram.Entry.e
     val pattern : cases_pattern_expr Gram.Entry.e
     val constr_pattern : constr_expr Gram.Entry.e
-(*
-    val ne_binders_list : local_binder list Gram.Entry.e
-*)
   end
 
 module Module : 
diff --git a/parsing/ppconstr.ml b/parsing/ppconstr.ml
index baac4a06d..e49f531f1 100644
--- a/parsing/ppconstr.ml
+++ b/parsing/ppconstr.ml
@@ -73,7 +73,12 @@ let wrap_exception = function
 
 let latom = 0
 let lannot = 1
-let lprod = 8
+let lprod = 1
+let llambda = 1
+let lif = 1
+let lletin = 1
+let lcases = 1
+let larrow = 8
 let lcast = 9
 let lapp = 10
 let ltop = (8,E)
@@ -98,7 +103,17 @@ 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 x = failwith "pr_delimiters: TODO"
+let pr_delimiters sc strm =
+  match find_delimiters sc with
+  | None -> anomaly "Delimiters without concrete syntax"
+  | Some (left,right) ->
+  assert (left <> "" && right <> "");
+  let lspace =
+    if is_letter (left.[String.length left -1]) then str " " else mt () in
+  let rspace =
+    let c = right.[0] in
+    if is_letter c or is_digit c or c = '\'' then str " " else mt () in
+  str left ++ lspace ++ strm ++ rspace ++ str right
 
 open Rawterm
 
@@ -118,7 +133,7 @@ let pr_explicitation = function
   | Some n -> int n ++ str "!"
 
 let pr_expl_args pr (a,expl) =
-  pr_explicitation expl ++ pr (latom,E) a
+  pr_explicitation expl ++ pr (lapp,L) a
 
 let pr_opt_type pr = function
   | CHole _ -> mt ()
@@ -197,8 +212,8 @@ let pr_fix pr = pr_recursive "Fix" (pr_fixdecl pr)
 let pr_cofix pr = pr_recursive "Fix" (pr_cofixdecl pr)
 
 let rec pr_arrow pr = function
-  | CArrow (_,a,b) -> pr (lprod,L) a ++ cut () ++ str "->" ++ pr_arrow pr b
-  | a -> pr (lprod,E) a
+  | CArrow (_,a,b) -> pr (larrow,L) a ++ cut () ++ str "->" ++ pr_arrow pr b
+  | a -> pr (larrow,E) a
 
 let pr_annotation pr t = str "<" ++ pr ltop t ++ str ">"
 
@@ -209,25 +224,26 @@ let rec pr inherited a =
   | CRef r -> pr_reference r, latom
   | CFix (_,id,fix) -> pr_fix pr (snd id) fix, latom
   | CCoFix (_,id,cofix) -> pr_cofix pr (snd id) cofix, latom
-  | CArrow _ -> hv 0 (pr_arrow pr a), lprod
+  | CArrow _ -> hv 0 (pr_arrow pr a), larrow
   | CProdN (_,bl,a) ->
       hov 0 (
 	str "(" ++ pr_binders pr bl ++ str ")" ++ brk(0,1) ++ pr ltop a), lprod
   | CLambdaN (_,bl,a) ->
       hov 0 (
-	str "[" ++ pr_binders pr bl ++ str "]" ++ brk(0,1) ++ pr ltop a), lprod
+	str "[" ++ pr_binders pr bl ++ str "]" ++ brk(0,1) ++ pr ltop a),
+      llambda
   | CLetIn (_,x,a,b) ->
-      hov 0 (pr_let_binder pr (snd x) a ++ cut () ++ pr ltop b), lprod
+      hov 0 (pr_let_binder pr (snd x) a ++ cut () ++ pr ltop b), lletin
   | CAppExpl (_,f,l) ->
       hov 0 (
-	str "!" ++ pr_reference f ++ 
-	prlist (fun a -> brk (1,1) ++ pr (latom,E) a) l), lapp
+	str "!" ++ pr_reference f ++
+	prlist (fun a -> brk (1,1) ++ pr (lapp,L) a) l), lapp
   | CApp (_,a,l) ->
       hov 0 (
 	pr (latom,E) a ++ 
 	prlist (fun a -> brk (1,1) ++ pr_expl_args pr a) l), lapp
   | CCases (_,po,c,eqns) ->
-      pr_cases po c eqns, lannot
+      pr_cases po c eqns, lcases
   | COrderedCase (_,IfStyle,po,c,[b1;b2]) ->
       (* On force les parenthèses autour d'un "if" sous-terme (même si le
 	 parsing est lui plus tolérant) *)
@@ -236,7 +252,7 @@ let rec pr inherited a =
 	hv 0 (
 	  str "if" ++ pr ltop c ++ spc () ++
 	  hov 0 (str "then" ++ brk (1,1) ++ pr ltop b1) ++ spc () ++
-	  hov 0 (str "else" ++ brk (1,1) ++ pr ltop b2))), lapp
+	  hov 0 (str "else" ++ brk (1,1) ++ pr ltop b2))), lif
   | COrderedCase (_,LetStyle,po,c,[CLambdaN(_,[_,_ as bd],b)]) ->
       hov 0 (
 	pr_opt (pr_annotation pr) po ++
@@ -245,7 +261,7 @@ let rec pr inherited a =
 	  hov 0 (str "(" ++ pr_binder pr bd ++ str ")") ++
 	  str "=" ++ brk (1,1) ++
 	  pr ltop c ++ spc () ++
-	  str "in " ++ pr ltop b)), lapp
+	  str "in " ++ pr ltop b)), lletin
   | COrderedCase (_,(MatchStyle|RegularStyle as style),po,c,bl) ->
       hov 0 (
 	hov 0 (
@@ -256,7 +272,7 @@ let rec pr inherited a =
 	    str (if style=RegularStyle then "of" else "with") ++
 	  brk (1,3) ++
 	  hov 0 (prlist (fun b -> pr ltop b ++ fnl ()) bl)) ++
-	str "end")), lannot
+	str "end")), lcases
   | COrderedCase (_,_,_,_,_) -> 
       anomaly "malformed if or destructuring let"
   | CHole _ -> str "?", latom
@@ -267,8 +283,7 @@ let rec pr inherited a =
   | CNotation (_,s,env) -> pr_notation pr s env
   | CGrammar _ -> failwith "CGrammar: TODO"
   | CNumeral (_,p) -> Bignat.pr_bigint p, latom
-  | CDelimiters (_,sc,a) -> failwith "pr_delim: TODO"
-(*      pr_delimiters (find_delimiters) (pr_constr_expr a)*)
+  | CDelimiters (_,sc,a) -> pr_delimiters sc (pr ltop a), latom
   | CDynamic _ -> str "<dynamic>", latom
   in
   if prec_less prec inherited then strm
@@ -352,8 +367,10 @@ let gentermpr gt =
 (* [at_top] means ids of env must be avoided in bound variables *)
 let gentermpr_core at_top env t =
   gentermpr (Termast.ast_of_constr at_top env t)
+
 (*
 let gentermpr_core at_top env t =
   pr_constr (Constrextern.extern_constr at_top env t)
 *)
 
+
diff --git a/parsing/printer.ml b/parsing/printer.ml
index 6305cd650..7777ac540 100644
--- a/parsing/printer.ml
+++ b/parsing/printer.ml
@@ -76,7 +76,10 @@ let pr_ref_label = function (* On triche sur le contexte *)
   | VarNode id -> pr_id id
 
 let pr_cases_pattern t = gentermpr (Termast.ast_of_cases_pattern t)
+(*
 let pr_rawterm t = gentermpr (Termast.ast_of_rawconstr t)
+*)
+let pr_rawterm t = pr_constr (Constrextern.extern_rawconstr t)
 let pr_pattern_env tenv env t = gentermpr (Termast.ast_of_pattern tenv env t)
 let pr_pattern t = pr_pattern_env (Global.env()) empty_names_context t