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

11 files changed, 154 insertions, 111 deletions

diff --git a/parsing/egrammar.ml b/parsing/egrammar.ml
index 17d973621..6e8cfb05b 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 859b5548a..1fa852362 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 70704f019..2cde3e24e 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 771434ea3..e55a41797 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 a7b27de23..7e1cf5da7 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 6476cec51..c298b0e3f 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 1d7519c99..e94b513fb 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 fa0c3809e..1a7df020c 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 d46a245ce..467fe5f33 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 e49f531f1..e177bb621 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 d963d8644..efcb5c8af 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