Mise en place de 'Scope' pour gérer des ensembles de notations - phase 1; hack temporaire autour du printer

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

19 files changed, 871 insertions, 228 deletions

diff --git a/parsing/ast.ml b/parsing/ast.ml
index a41e627e6e..52a390af1f 100755
--- a/parsing/ast.ml
+++ b/parsing/ast.ml
@@ -13,7 +13,6 @@ open Util
 open Names
 open Libnames
 open Coqast
-open Tacexpr
 open Genarg
 
 let isMeta s = String.length s <> 0 & s.[0]='$'
@@ -239,7 +238,9 @@ let coerce_reference_to_id = function
 
 let slam_ast (_,fin) id ast =
   match id with
-    | Coqast.Nvar ((deb,_), s) -> Coqast.Slam ((deb,fin), Some s, ast)
+    | Coqast.Nvar ((deb,_), s) -> 
+	let name = if s = id_of_string "_" then None else Some s in
+	Coqast.Slam ((deb,fin), name, ast)
     | Coqast.Nmeta ((deb,_), s) -> Coqast.Smetalam ((deb,fin), s, ast)
     | _ -> invalid_arg "Ast.slam_ast"
 
@@ -269,7 +270,7 @@ let env_assoc_value loc v env =
   with Not_found -> 
     anomaly_loc
       (loc,"Ast.env_assoc_value",
-       (str"metavariable " ++ str v ++ str" is unbound."))
+       (str"metavariable " ++ str v ++ str" is unbound"))
 
 let env_assoc_list sigma (loc,v) =
   match env_assoc_value loc v sigma with
@@ -404,7 +405,7 @@ let typed_ast_match env p a = match (p,a) with
 
 let astl_match = amatchl []
 
-let ast_first_match pat_of_fun env ast sl =
+let first_match pat_of_fun env ast sl =
   let rec aux = function
     | [] -> None
     | h::t ->
@@ -413,12 +414,13 @@ let ast_first_match pat_of_fun env ast sl =
   in 
   aux sl
 
-let first_match pat_of_fun env ast sl =
+let find_all_matches pat_of_fun env ast sl =
   let rec aux = function
-    | [] -> None
+    | [] -> []
     | (h::t) ->
-        (try Some (h, ast_match env (pat_of_fun h) ast)
-         with (No_match _| Stdpp.Exc_located (_,No_match _)) -> aux t)
+        let l = aux t in
+        (try (h, ast_match env (pat_of_fun h) ast)::l
+         with (No_match _| Stdpp.Exc_located (_,No_match _)) -> l)
   in 
   aux sl
 
@@ -695,7 +697,7 @@ let rec eval_act dloc sigma = function
   | ActCase(e,ml) ->
       (match eval_act dloc sigma e with
         | (PureAstNode esub) ->
-            (match ast_first_match myfst sigma esub ml with
+            (match first_match myfst sigma esub ml with
               | Some((_,a),sigma_pat) -> eval_act dloc sigma_pat a
               | _ -> case_failed dloc sigma esub (List.map myfst ml))
         | _ -> grammar_type_error (dloc,"Ast.eval_act"))
diff --git a/parsing/ast.mli b/parsing/ast.mli
index 07dbd06f29..9fd8e9cc92 100755
--- a/parsing/ast.mli
+++ b/parsing/ast.mli
@@ -103,7 +103,7 @@ val coerce_to_id : Coqast.t -> identifier
 
 val coerce_qualid_to_id : qualid Util.located -> identifier
 
-val coerce_reference_to_id : Tacexpr.reference_expr -> identifier
+val coerce_reference_to_id : reference_expr -> identifier
 
 val abstract_binders_ast :
   Coqast.loc -> string -> Coqast.t -> Coqast.t -> Coqast.t
@@ -144,7 +144,7 @@ val replace_vars_ast : (identifier * identifier) list -> Coqast.t -> Coqast.t
 val bind_env : env -> string -> typed_ast -> env
 val ast_match : env -> astpat -> Coqast.t -> env
 val astl_match : env -> patlist -> Coqast.t list -> env
-val first_match : ('a -> astpat) -> env -> t -> 'a list -> ('a * env) option
+val find_all_matches : ('a -> astpat) -> env -> t -> 'a list -> ('a * env) list
 val first_matchl : ('a -> patlist) -> env -> Coqast.t list -> 'a list ->
   ('a * env) option
 
diff --git a/parsing/astterm.ml b/parsing/astterm.ml
index 89025de4f4..03e652ccea 100644
--- a/parsing/astterm.ml
+++ b/parsing/astterm.ml
@@ -196,7 +196,7 @@ let maybe_constructor allow_var env = function
       let qid = interp_qualid l in
       (try match extended_locate qid with
        | SyntacticDef sp ->
-	   (match Syntax_def.search_syntactic_definition sp with
+	   (match Syntax_def.search_syntactic_definition loc sp with
 	    | RRef (_,(ConstructRef c as x)) ->
 		if !dump then add_glob loc x; 
  		ConstrPat (loc,c)
@@ -267,7 +267,7 @@ let ast_to_global loc c =
     | ("EVAR", [(Num (_,ev))]) ->
 	REvar (loc, ev), []
     | ("SYNCONST", [sp]) ->
-	Syntax_def.search_syntactic_definition (ast_to_sp sp), []
+	Syntax_def.search_syntactic_definition loc (ast_to_sp sp), []
     | _ -> anomaly_loc (loc,"ast_to_global",
 			(str "Bad ast for this global a reference"))
 
@@ -285,7 +285,7 @@ let ref_from_constr c = match kind_of_term c with
    [vars2] is the set of global variables, env is the set of variables
    abstracted until this point *)
 
-let ast_to_var (env,impls) (vars1,vars2) loc id =
+let ast_to_var (env,impls,_) (vars1,vars2) loc id =
   let imps =
     if Idset.mem id env or List.mem id vars1
     then
@@ -322,7 +322,7 @@ let rawconstr_of_qualid env vars loc qid =
     let imps = implicits_of_global ref in
     RRef (loc, ref), imps
   | SyntacticDef sp ->
-    set_loc_of_rawconstr loc (Syntax_def.search_syntactic_definition sp), []
+    Syntax_def.search_syntactic_definition loc sp, []
   with Not_found ->
     error_global_not_found_loc loc qid
 
@@ -352,7 +352,7 @@ let message_redundant_alias (s1,s2) =
   warning ("Alias variable "^(string_of_id s1)
 	   ^" is merged with "^(string_of_id s2))
 
-let rec ast_to_pattern env aliases = function
+let rec ast_to_pattern (_,_,scopes as env) aliases = function
   | Node(_,"PATTAS",[Nvar (loc,s); p]) ->
       let aliases' = merge_aliases aliases (name_of_nvar s) in
       ast_to_pattern env aliases' p
@@ -369,6 +369,16 @@ let rec ast_to_pattern env aliases = function
 	     user_err_loc (loc,"ast_to_pattern",mssg_hd_is_not_constructor s)
 *)
               assert false)
+  | Node(_,"PATTNUMERAL", [Str(loc,n)]) ->
+      ([aliases],
+      Symbols.interp_numeral_as_pattern loc (Bignat.POS (Bignat.of_string n))
+	(alias_of aliases) scopes)
+
+  | Node(_,"PATTNEGNUMERAL", [Str(loc,n)]) ->
+      ([aliases],
+      Symbols.interp_numeral_as_pattern loc (Bignat.NEG (Bignat.of_string n))
+	(alias_of aliases) scopes)
+
   | ast ->
       (match maybe_constructor true env ast with
 	 | ConstrPat (loc,c) -> ([aliases], PatCstr (loc,c,[],alias_of aliases))
@@ -420,8 +430,17 @@ let set_hole_implicit i = function
   | RVar (loc,id) -> (loc,ImplicitArg (VarRef id,i))
   | _ -> anomaly "Only refs have implicits"
 
+let build_expression loc1 loc2 (ref,impls) args =
+  let rec add_args n = function
+    | true::impls,args -> (RHole (set_hole_implicit n (RRef (loc2,ref))))::add_args (n+1) (impls,args)
+    | false::impls,a::args -> a::add_args (n+1) (impls,args)
+    | [], args -> args
+    | _ -> anomalylabstrm "astterm"
+      (str "Incorrect signature " ++ pr_global_env None ref ++ str " as an infix") in
+  RApp (loc1,RRef (loc2,ref),add_args 1 (impls,args))
+
 let ast_to_rawconstr sigma env allow_soapp lvar =
-  let rec dbrec (ids,impls as env) = function
+  let rec dbrec (ids,impls,scopes as env) = function
     | Nvar(loc,s) ->
 	fst (rawconstr_of_var env lvar loc s)
 
@@ -436,7 +455,7 @@ let ast_to_rawconstr sigma env allow_soapp lvar =
           with Not_found ->
 	    error_fixname_unbound "ast_to_rawconstr (FIX)" false locid iddef in
 	let ext_ids = List.fold_right Idset.add lf ids in
-	let defl = Array.of_list (List.map (dbrec (ext_ids,impls)) lt) in
+	let defl = Array.of_list (List.map (dbrec (ext_ids,impls,scopes)) lt) in
 	let arityl = Array.of_list (List.map (dbrec env) lA) in
 	RRec (loc,RFix (Array.of_list ln,n), Array.of_list lf, arityl, defl)
 	  
@@ -449,7 +468,7 @@ let ast_to_rawconstr sigma env allow_soapp lvar =
 	    error_fixname_unbound "ast_to_rawconstr (COFIX)" true locid iddef
 	in
 	let ext_ids = List.fold_right Idset.add lf ids in
-	let defl = Array.of_list (List.map (dbrec (ext_ids,impls)) lt) in
+	let defl = Array.of_list (List.map (dbrec (ext_ids,impls,scopes)) lt) in
 	let arityl = Array.of_list (List.map (dbrec env) lA) in
 	RRec (loc,RCoFix n, Array.of_list lf, arityl, defl)
 	  
@@ -457,7 +476,7 @@ let ast_to_rawconstr sigma env allow_soapp lvar =
 	let na,ids' = match ona with
 	  | Some id -> Name id, Idset.add id ids
 	  | _ -> Anonymous, ids in
-	let c1' = dbrec env c1 and c2' = dbrec (ids',impls) c2 in
+	let c1' = dbrec env c1 and c2' = dbrec (ids',impls,scopes) c2 in
 	(match k with
 	   | "PROD" -> RProd (loc, na, c1', c2')
 	   | "LAMBDA" -> RLambda (loc, na, locate_if_isevar locna na c1', c2')
@@ -467,6 +486,20 @@ let ast_to_rawconstr sigma env allow_soapp lvar =
     | Node(_,("PRODLIST"|"LAMBDALIST" as s), [c1;(Slam _ as c2)]) -> 
 	iterated_binder s 0 c1 env c2
 
+    | Node(loc1,"NOTATION", Str(loc2,ntn)::args) ->
+	Symbols.interp_notation ntn scopes (List.map (dbrec env) args)
+
+    | Node(_,"NUMERAL", [Str(loc,n)]) ->
+	Symbols.interp_numeral loc (Bignat.POS (Bignat.of_string n))
+	  scopes
+
+    | Node(_,"NEGNUMERAL", [Str(loc,n)]) ->
+	Symbols.interp_numeral loc (Bignat.NEG (Bignat.of_string n))
+	  scopes
+
+    | Node(_,"DELIMITERS", [Str(_,sc);e]) ->
+	dbrec (ids,impls,sc::scopes) e
+
     | Node(loc,"APPLISTEXPL", f::args) ->
 	RApp (loc,dbrec env f,ast_to_args env args)
 
@@ -536,7 +569,7 @@ let ast_to_rawconstr sigma env allow_soapp lvar =
 
     | _ -> anomaly "ast_to_rawconstr: unexpected ast"
 
-  and ast_to_eqn n (ids,impls as env) = function
+  and ast_to_eqn n (ids,impls,scopes as env) = function
     | Node(loc,"EQN",rhs::lhs) ->
 	let (idsl_substl_list,pl) =
 	  List.split (List.map (ast_to_pattern env ([],[])) lhs) in
@@ -550,10 +583,10 @@ let ast_to_rawconstr sigma env allow_soapp lvar =
 	let rhs = replace_vars_ast subst rhs in
 	List.iter message_redundant_alias subst;
 	let env_ids = List.fold_right Idset.add eqn_ids ids in
-	(loc, eqn_ids,pl,dbrec (env_ids,impls) rhs)
+	(loc, eqn_ids,pl,dbrec (env_ids,impls,scopes) rhs)
     | _ -> anomaly "ast_to_rawconstr: ill-formed ast for Cases equation"
 
-  and iterated_binder oper n ty (ids,impls as env) = function
+  and iterated_binder oper n ty (ids,impls,scopes as env) = function
     | Slam(loc,ona,body) ->
 	let na,ids' = match ona with 
 	  | Some id ->
@@ -561,7 +594,7 @@ let ast_to_rawconstr sigma env allow_soapp lvar =
 	      Name id, Idset.add id ids
 	  | _ -> Anonymous, ids
 	in
-	let r = iterated_binder oper (n+1) ty (ids',impls) body in
+	let r = iterated_binder oper (n+1) ty (ids',impls,scopes) body in
 	(match oper with
 	   | "PRODLIST" -> RProd(loc, na, dbrec env ty, r)
 	   | "LAMBDALIST" ->
@@ -715,7 +748,7 @@ let globalize_ast ast =
 
 let interp_rawconstr_gen sigma env impls allow_soapp lvar com =
   ast_to_rawconstr sigma
-    (from_list (ids_of_rel_context (rel_context env)), impls)
+    (from_list (ids_of_rel_context (rel_context env)), impls, Symbols.current_scopes ())
     allow_soapp (lvar,env) com
 
 let interp_rawconstr sigma env com =
@@ -748,7 +781,7 @@ let constrOut = function
       (str "Not a Dynamic ast: " ++ print_ast ast)
 
 let interp_global_constr env (loc,qid) = 
-  let c,_ = rawconstr_of_qualid (Idset.empty,[]) ([],env) loc qid in
+  let c,_ = rawconstr_of_qualid (Idset.empty,[],Symbols.current_scopes()) ([],env) loc qid in
   understand Evd.empty env c
 
 let interp_constr sigma env c =
@@ -869,7 +902,7 @@ let pattern_of_rawconstr lvar c =
 let interp_constrpattern_gen sigma env lvar com = 
   let c =
     ast_to_rawconstr sigma
-      (from_list (ids_of_rel_context (rel_context env)), [])
+      (from_list (ids_of_rel_context (rel_context env)), [], Symbols.current_scopes ())
       true (List.map fst lvar,env) com
   and nlvar = List.map (fun (id,c) -> (id,pattern_of_constr c)) lvar in
   try 
diff --git a/parsing/coqlib.ml b/parsing/coqlib.ml
index 96743098cf..5c0fef4aa9 100644
--- a/parsing/coqlib.ml
+++ b/parsing/coqlib.ml
@@ -34,8 +34,10 @@ let nat_path = make_path datatypes_module (id_of_string "nat")
 
 let glob_nat = IndRef (nat_path,0)
 
-let glob_O = ConstructRef ((nat_path,0),1)
-let glob_S = ConstructRef ((nat_path,0),2)
+let path_of_O = ((nat_path,0),1)
+let path_of_S = ((nat_path,0),2)
+let glob_O = ConstructRef path_of_O
+let glob_S = ConstructRef path_of_S
 
 let eq_path = make_path logic_module (id_of_string "eq")
 let eqT_path = make_path logic_type_module (id_of_string "eqT")
diff --git a/parsing/coqlib.mli b/parsing/coqlib.mli
index 8eedab0500..dbe99e3991 100644
--- a/parsing/coqlib.mli
+++ b/parsing/coqlib.mli
@@ -27,6 +27,8 @@ val logic_type_module : dir_path
 
 (* Natural numbers *)
 val glob_nat : global_reference
+val path_of_O : constructor
+val path_of_S : constructor
 val glob_O : global_reference
 val glob_S : global_reference
 
diff --git a/parsing/esyntax.ml b/parsing/esyntax.ml
index b3d0278028..9f802563b8 100644
--- a/parsing/esyntax.ml
+++ b/parsing/esyntax.ml
@@ -18,6 +18,7 @@ open Extend
 open Vernacexpr
 open Names
 open Nametab
+open Symbols
 
 (*** Syntax keys ***)
 
@@ -114,7 +115,7 @@ let find_syntax_entry whatfor gt =
     List.flatten
       (List.map (fun k -> Gmapl.find (whatfor,k) !from_key_table) gt_keys)
   in 
-  first_match (fun se -> se.syn_astpat) [] gt entries
+  find_all_matches (fun se -> se.syn_astpat) [] gt entries
 
 let remove_with_warning name =
   if Gmap.mem name !from_name_table then begin
@@ -139,10 +140,9 @@ let add_ppobject {sc_univ=wf;sc_entries=sel} = List.iter (add_rule wf) sel
 
 (* Pretty-printing machinery *)
 
-type std_printer = Coqast.t -> std_ppcmds
+type std_printer = Genarg.constr_ast -> std_ppcmds
 type unparsing_subfunction = string -> tolerability option -> std_printer
-
-type std_constr_printer = Genarg.constr_ast -> std_ppcmds
+type primitive_printer = Genarg.constr_ast -> std_ppcmds option
 
 (* Module of primitive printers *)
 module Ppprim =
@@ -153,94 +153,111 @@ module Ppprim =
     let add (a,ppr) = tab := (a,ppr)::!tab
   end
 
-(* A printer for the tokens. *)
-let token_printer stdpr = function
-  | (Id _ | Num _ | Str _ | Path _ as ast) -> print_ast ast
-  | a -> stdpr a
+(**********************************************************************)
+(* Primitive printers (e.g. for numerals)                             *)
+
+(* This is the map associating to a printer the scope it belongs to   *)
+(* and its ML code                                                    *)
+
+let primitive_printer_tab = 
+  ref (Stringmap.empty : (scope_name * primitive_printer) Stringmap.t)
+let declare_primitive_printer s sc pp =
+  primitive_printer_tab := Stringmap.add s (sc,pp) !primitive_printer_tab
+let lookup_primitive_printer s =
+  Stringmap.find s !primitive_printer_tab
 
 (* Register the primitive printer for "token". It is not used in syntax/PP*.v,
  * but any ast matching no PP rule is printed with it. *)
+(*
+let _ = declare_primitive_printer "token" token_printer
+*)
 
-let _ = Ppprim.add ("token",token_printer)
+(* A printer for the tokens. *)
+let token_printer stdpr = function
+  | (Id _ | Num _ | Str _ | Path _ as ast) -> print_ast ast
+  | a -> stdpr a
 
 (* A primitive printer to do "print as" (to specify a length for a string) *)
-let print_as_printer stdpr = function
-  | Node (_, "AS", [Num(_,n); Str(_,s)]) -> stras (n,s)
-  | ast                                  -> stdpr ast
+let print_as_printer = function
+  | Node (_, "AS", [Num(_,n); Str(_,s)]) -> Some (stras (n,s))
+  | ast                                  -> None
 
-let _ = Ppprim.add ("print_as",print_as_printer)
+let _ = declare_primitive_printer "print_as" default_scope print_as_printer
 
 (* Handle infix symbols *)
 
-let find_infix_symbols sp =
-  try Spmap.find sp !infix_names_map with Not_found -> []
-
-let find_infix_name a =
-  try Stringmap.find a !infix_symbols_map
-  with Not_found -> anomaly ("Undeclared symbol: "^a)
-
-let declare_infix_symbol sp s =
-  let l = find_infix_symbols sp in
-  infix_names_map := Spmap.add sp (s::l) !infix_names_map;
-  infix_symbols_map := Stringmap.add s sp !infix_symbols_map
-
-let meta_pattern m = Pmeta(m,Tany)
-
-let make_hunks (lp,rp) s e1 e2 =
-  let n,s =
-    if is_letter (s.[String.length s -1]) or is_letter (s.[0])
-    then 1,s^" " else 0,s
-  in
-  [PH (meta_pattern e1, None, lp);
-   UNP_BRK (n, 1); RO s;
-   PH (meta_pattern e2, None, rp)]
-
-let build_syntax (ref,e1,e2,assoc) =
-  let sp = match ref with
-  | TrueGlobal r -> Nametab.sp_of_global None r
-  | SyntacticDef kn -> Nametab.sp_of_syntactic_definition kn in
-  let rec find_symbol = function
-    | [] ->
-	let s = match ref with
-	  | TrueGlobal r ->
-	      string_of_qualid (shortest_qualid_of_global None r)
-	  | SyntacticDef _ -> string_of_path sp in
-	UNP_BOX (PpHOVB 0,
-	  [RO "("; RO s; UNP_BRK (1, 1); PH (meta_pattern e1, None, E);
-	   UNP_BRK (1, 1); PH (meta_pattern e2, None, E); RO ")"])
-    | a::l ->
-	if find_infix_name a = sp then
-	  UNP_BOX (PpHOVB 1, make_hunks assoc a e1 e2)
-	else
-	  find_symbol l
-  in find_symbol (find_infix_symbols sp)
-
+let pr_parenthesis inherited se strm =
+  let rule_prec = (se.syn_id, se.syn_prec) in
+  let no_paren = tolerable_prec inherited rule_prec in
+  if no_paren then 
+    strm
+  else 
+    (str"(" ++ strm ++ str")")
+    
+let print_delimiters inh se strm = function
+  | None -> pr_parenthesis inh se strm
+  | 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
 
 (* Print the syntax entry. In the unparsing hunks, the tokens are
  * printed using the token_printer, unless another primitive printer
  * is specified. *)
 
-let print_syntax_entry whatfor sub_pr env se = 
-  let rule_prec = (se.syn_id, se.syn_prec) in
-  let rec print_hunk = function
+let print_syntax_entry sub_pr scopes env se = 
+  let rec print_hunk rule_prec scopes = function
     | PH(e,externpr,reln) ->
 	let node = Ast.pat_sub Ast.dummy_loc env e in
 	let printer =
 	  match externpr with (* May branch to an other printer *)
 	    | Some c ->
                 (try (* Test for a primitive printer *) Ppprim.map c
-                with Not_found -> token_printer )
+                with Not_found -> token_printer)
 	    | _ -> token_printer in
-	printer (sub_pr whatfor (Some(rule_prec,reln))) node
+	printer (sub_pr scopes (Some(rule_prec,reln))) node
     | RO s -> str s
     | UNP_TAB -> tab ()
     | UNP_FNL -> fnl ()
     | UNP_BRK(n1,n2) -> brk(n1,n2)
     | UNP_TBRK(n1,n2) -> tbrk(n1,n2)
-    | UNP_BOX (b,sub) -> ppcmd_of_box b (prlist print_hunk sub)
-    | UNP_INFIX (sp,e1,e2,assoc) -> print_hunk (build_syntax (sp,e1,e2,assoc))
+    | UNP_BOX (b,sub) -> ppcmd_of_box b (prlist (print_hunk rule_prec scopes) sub)
+    | UNP_SYMBOLIC _ -> anomaly "handled by call_primitive_parser"
   in 
-  prlist print_hunk se.syn_hunks
+  let rule_prec = (se.syn_id, se.syn_prec) in
+  prlist (print_hunk rule_prec scopes) se.syn_hunks
+
+let call_primitive_parser rec_pr otherwise inherited scopes (se,env) =
+  try (
+  match se.syn_hunks with
+    | [PH(e,Some c,reln)] ->
+	  (* 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
+	    | None -> otherwise ()
+	    | Some (dlm,scopes) ->
+	        (* We can use this printer *)
+	        let node = Ast.pat_sub Ast.dummy_loc env e in
+	        match pr node with
+		  | Some strm -> print_delimiters inherited se strm dlm
+		  | None -> otherwise ())
+    | [UNP_SYMBOLIC (sc,pat,sub)] ->
+	(match Symbols.find_notation sc pat scopes with
+	  | None -> otherwise ()
+	  | Some (dlm,scopes) ->
+	      print_delimiters inherited se
+		(print_syntax_entry rec_pr scopes env 
+		  {se with syn_hunks = [sub]}) dlm)
+    | _ ->
+	pr_parenthesis inherited se (print_syntax_entry rec_pr scopes env se)
+  )
+  with Not_found -> (* To handle old style printer *)
+	pr_parenthesis inherited se (print_syntax_entry rec_pr scopes env se)
 
 (* [genprint whatfor dflt inhprec ast] prints out the ast of
  * 'universe' whatfor. If the term is not matched by any
@@ -250,20 +267,19 @@ let print_syntax_entry whatfor sub_pr env se =
  * global constants basenames. *)
 
 let genprint dflt whatfor inhprec ast =
-  let rec rec_pr whatfor inherited gt =
-    match find_syntax_entry whatfor gt with
-      | Some(se, env) ->     
-	  let rule_prec = (se.syn_id, se.syn_prec) in
-	  let no_paren = tolerable_prec inherited rule_prec in
-	  let printed_gt = print_syntax_entry whatfor rec_pr env se in
-	  if no_paren then 
-	    printed_gt
-	  else 
-	    (str"(" ++ printed_gt ++ str")")
-      | None -> dflt gt (* No rule found *)
+  let rec rec_pr scopes inherited gt =
+    let entries = find_syntax_entry whatfor gt in
+    let rec test_rule = function
+      | se_env::rules ->
+	  call_primitive_parser
+	    rec_pr 
+	    (fun () -> test_rule rules) 
+	    inherited scopes se_env
+      | [] -> dflt gt (* No rule found *)
+    in test_rule entries
   in
   try 
-    rec_pr whatfor inhprec ast
+    rec_pr (Symbols.current_scopes ()) inhprec ast
   with
     | Failure _ -> (str"<PP failure: " ++ dflt ast ++ str">")
     | Not_found -> (str"<PP search failure: " ++ dflt ast ++ str">")
diff --git a/parsing/esyntax.mli b/parsing/esyntax.mli
index 8e3445ed76..cf1b0de3f7 100644
--- a/parsing/esyntax.mli
+++ b/parsing/esyntax.mli
@@ -12,6 +12,7 @@
 open Pp
 open Extend
 open Vernacexpr
+open Symbols
 (*i*)
 
 (* Syntax entry tables. *)
@@ -25,27 +26,37 @@ val unfreeze : frozen_t -> unit
 
 (* Search and add a PP rule for an ast in the summary *)
 val find_syntax_entry :
-  string -> Coqast.t -> (Ast.astpat syntax_entry * Ast.env) option
+  string -> Coqast.t -> (Ast.astpat syntax_entry * Ast.env) list
 val add_rule : string -> Ast.astpat syntax_entry -> unit
 val add_ppobject : Ast.astpat syntax_command -> unit
 val warning_verbose : bool ref
 
 (* Pretty-printing *)
 
-type std_printer = Coqast.t -> std_ppcmds
+type std_printer = Genarg.constr_ast -> std_ppcmds
 type unparsing_subfunction = string -> tolerability option -> std_printer
+type primitive_printer = Genarg.constr_ast -> std_ppcmds option
 
-(* Module of constr primitive printers *)
+(* Module of constr primitive printers [old style - no scope] *)
 module Ppprim :
   sig
     type t = std_printer -> std_printer
     val add : string * t -> unit
   end
 
+val declare_primitive_printer : 
+  string -> scope_name -> primitive_printer -> unit
+
+(*
 val declare_infix_symbol : Libnames.section_path -> string -> unit
+*)
 
 (* Generic printing functions *) 
+(*
 val token_printer: std_printer -> std_printer
+*)
+(*
 val print_syntax_entry : 
   string -> unparsing_subfunction -> Ast.env -> Ast.astpat syntax_entry -> std_ppcmds
+*)
 val genprint : std_printer -> unparsing_subfunction
diff --git a/parsing/extend.ml b/parsing/extend.ml
index 7c4c400ebb..a469a648f8 100644
--- a/parsing/extend.ml
+++ b/parsing/extend.ml
@@ -187,8 +187,7 @@ type 'pat unparsing_hunk =
   | UNP_TBRK of int * int
   | UNP_TAB
   | UNP_FNL
-  | UNP_INFIX of Libnames.extended_global_reference * string * string *
-      (parenRelation * parenRelation)
+  | UNP_SYMBOLIC of string * string * 'pat unparsing_hunk
 
 let rec subst_hunk subst_pat subst hunk = match hunk with
   | PH (pat,so,pr) ->
@@ -204,10 +203,10 @@ let rec subst_hunk subst_pat subst hunk = match hunk with
   | UNP_TBRK _
   | UNP_TAB
   | UNP_FNL -> hunk
-  | UNP_INFIX (ref,s1,s2,prs) ->
-      let ref' = Libnames.subst_ext subst ref in
-	if ref' == ref then hunk else
-	  UNP_INFIX (ref',s1,s2,prs)
+  | UNP_SYMBOLIC (s1, s2, pat) ->
+      let pat' = subst_hunk subst_pat subst pat in
+	if pat' == pat then hunk else
+	  UNP_SYMBOLIC (s1, s2, pat')
 
 (* Checks if the precedence of the parent printer (None means the
    highest precedence), and the child's one, follow the given
@@ -271,8 +270,8 @@ type syntax_entry_ast = precedence * syntax_rule list
 let rec interp_unparsing env = function
   | PH (ast,ext,pr) -> PH (Ast.val_of_ast env ast,ext,pr)
   | UNP_BOX (b,ul) -> UNP_BOX (b,List.map (interp_unparsing env) ul)
-  | UNP_BRK _ | RO _ | UNP_TBRK _ | UNP_TAB | UNP_FNL
-  | UNP_INFIX _ as x -> x
+  | UNP_BRK _ | RO _ | UNP_TBRK _ | UNP_TAB | UNP_FNL as x -> x
+  | UNP_SYMBOLIC (x,y,u) -> UNP_SYMBOLIC (x,y,interp_unparsing env u)
 
 let rule_of_ast univ prec (s,spat,unp) =
   let (astpat,meta_env) = Ast.to_pat [] spat in
diff --git a/parsing/extend.mli b/parsing/extend.mli
index 8734e34525..7294a2bb0d 100644
--- a/parsing/extend.mli
+++ b/parsing/extend.mli
@@ -82,8 +82,11 @@ type 'pat unparsing_hunk =
   | UNP_TBRK of int * int
   | 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) -> 
diff --git a/parsing/g_basevernac.ml4 b/parsing/g_basevernac.ml4
index ede831944e..bac4892179 100644
--- a/parsing/g_basevernac.ml4
+++ b/parsing/g_basevernac.ml4
@@ -94,10 +94,10 @@ GEXTEND Gram
 	  VernacSearch (SearchRewrite c, l)
 
       (* TODO: rapprocher Eval et Check *)
-      | IDENT "Eval"; g = OPT natural; r = Tactic.red_expr; "in";
-	  c = constr -> VernacCheckMayEval (Some r, g, c)
-      | IDENT "Check"; g = OPT natural; c = constr ->
-	  VernacCheckMayEval (None, g, c)
+      | IDENT "Eval"; r = Tactic.red_expr; "in";
+	  c = constr -> VernacCheckMayEval (Some r, None, c)
+      | IDENT "Check"; c = constr ->
+	  VernacCheckMayEval (None, None, c)
       | "Type"; c = constr -> VernacGlobalCheck c      (* pas dans le RefMan *)
 
       | IDENT "Add"; IDENT "ML"; IDENT "Path"; dir = STRING ->
@@ -218,10 +218,18 @@ GEXTEND Gram
      | "Syntax"; u = univ; el = LIST1 syntax_entry SEP ";" ->
          VernacSyntax (u,el)
 
+     | IDENT "Open"; IDENT "Scope"; sc = IDENT -> VernacOpenScope sc
+
+     | IDENT "Delimiters"; left = STRING; sc = IDENT; right = STRING ->
+	 VernacDelimiters (sc,(left,right))
+
      (* Faudrait une version de qualidarg dans Prim pour respecter l'ordre *)
-     | IDENT "Infix"; a = entry_prec; n = natural; op = STRING; p = qualid
-        -> VernacInfix (a,n,op,p)
-     | IDENT "Distfix"; a = entry_prec; n = natural; s = STRING; p = qualid        -> VernacDistfix (a,n,s,p)
+     | IDENT "Infix"; a = entry_prec; n = natural; op = STRING; p = qualid;
+	 sc = OPT [ ":"; sc = IDENT -> sc ] -> VernacInfix (a,n,op,p,sc)
+     | IDENT "Distfix"; a = entry_prec; n = natural; s = STRING; p = qualid;
+	 sc = OPT [ ":"; sc = IDENT -> sc ] -> VernacDistfix (a,n,s,p,sc)
+     | IDENT "Notation"; a = entry_prec; n = natural; s = STRING; c = constr;
+	 sc = OPT [ ":"; sc = IDENT -> sc ] -> VernacNotation (a,n,s,c,sc)
 
      (* "Print" "Grammar" should be here but is in "command" entry in order 
         to factorize with other "Print"-based vernac entries *)
diff --git a/parsing/g_cases.ml4 b/parsing/g_cases.ml4
index 1ba2c6f233..6bee39b122 100644
--- a/parsing/g_cases.ml4
+++ b/parsing/g_cases.ml4
@@ -18,7 +18,12 @@ GEXTEND Gram
 
   pattern:
     [ [ qid = global -> qid
-      | "("; p = compound_pattern; ")" -> p ] ]
+      | "("; p = compound_pattern; ")" -> p
+      | n = INT ->
+	  let n = Coqast.Str (loc,n) in <:ast< (PATTNUMERAL $n) >>
+      | "-"; n = INT ->
+	  let n = Coqast.Str (loc,n) in <:ast< (PATTNEGNUMERAL $n) >>
+    ] ]
   ;
   compound_pattern:
     [ [ p = pattern ; lp = ne_pattern_list ->
diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4
index cbe3a14c24..4f8cbaa8c7 100644
--- a/parsing/g_constr.ml4
+++ b/parsing/g_constr.ml4
@@ -17,7 +17,7 @@ GEXTEND Gram
   GLOBAL: constr0 constr1 constr2 constr3 lassoc_constr4 constr5
           constr6 constr7 constr8 constr9 constr10 lconstr constr
           ne_ident_comma_list ne_constr_list sort ne_binders_list qualid
-          global constr_pattern ident;
+          global constr_pattern ident numarg;
   ident:
     [ [ id = Prim.var -> id
 
@@ -94,6 +94,10 @@ GEXTEND Gram
           <:ast< (COFIX $id ($LIST $fbinders)) >>
       | s = sort -> s
       | v = global -> v
+      | n = INT ->
+	  let n = Coqast.Str (loc,n) in <:ast< (NUMERAL $n) >>
+      | "-"; n = INT ->
+	  let n = Coqast.Str (loc,n) in <:ast< (NEGNUMERAL $n) >>
   ] ]
   ;
   constr1:
@@ -169,9 +173,12 @@ GEXTEND Gram
     [ [ c1 = constr8 -> c1
       | c1 = constr8; "::"; c2 = constr8 -> <:ast< (CAST $c1 $c2) >> ] ]
   ;
+  numarg:
+    [ [ n = Prim.natural -> Coqast.Num (loc, n) ] ]
+  ;
   simple_binding:
     [ [ id = ident; ":="; c = constr -> <:ast< (BINDING $id $c) >>
-      | n = Prim.numarg; ":="; c = constr -> <:ast< (BINDING $n $c) >> ] ]
+      | n = numarg; ":="; c = constr -> <:ast< (BINDING $n $c) >> ] ]
   ;
   simple_binding_list:
     [ [ b = simple_binding; l = simple_binding_list -> b :: l | -> [] ] ]
@@ -181,7 +188,7 @@ GEXTEND Gram
           Coqast.Node
             (loc, "EXPLICITBINDINGS",
              (Coqast.Node (loc, "BINDING", [Ast.coerce_to_var c1; c2]) :: bl))
-      | n = Prim.numarg; ":="; c = constr; bl = simple_binding_list ->
+      | n = numarg; ":="; c = constr; bl = simple_binding_list ->
           <:ast<(EXPLICITBINDINGS (BINDING $n $c) ($LIST $bl))>>
       | c1 = constr; bl = LIST0 constr ->
           <:ast<(IMPLICITBINDINGS $c1 ($LIST $bl))>> ] ]
@@ -234,9 +241,10 @@ GEXTEND Gram
       | -> <:ast< (ISEVAR) >> ] ]
   ;
   constr91:
-    [ [ n = Prim.natural; "!"; c1 = constr9 ->
-      let n = Coqast.Num (loc,n) in
-          <:ast< (EXPL $n $c1) >>
+    [ [ n = INT; "!"; c1 = constr9 ->
+          let n = Coqast.Num (loc,int_of_string n) in <:ast< (EXPL $n $c1) >>
+      | n = INT ->
+	  let n = Coqast.Str (loc,n) in <:ast< (NUMERAL $n) >>
       | c1 = constr9 -> c1 ] ]
   ;
   ne_constr91_list:
diff --git a/parsing/g_ltac.ml4 b/parsing/g_ltac.ml4
index fe6561b972..859865ee45 100644
--- a/parsing/g_ltac.ml4
+++ b/parsing/g_ltac.ml4
@@ -13,15 +13,17 @@
 open Pp
 open Util
 open Ast
-open Pcoq
 open Coqast
 open Rawterm
 open Tacexpr
 open Ast
-open Tactic
 
 ifdef Quotify then
 open Qast
+else
+open Pcoq
+
+open Tactic
 
 ifdef Quotify then
 open Q
@@ -31,26 +33,32 @@ type let_clause_kind =
   | LETCLAUSE of
       (Names.identifier Util.located * Genarg.constr_ast may_eval option * raw_tactic_arg)
 
-let fail_default_value = 0
-
-let out_letin_clause loc = function
-  | LETTOPCLAUSE _ -> user_err_loc (loc, "", (str "Syntax Error"))
-  | LETCLAUSE (id,c,d) -> (id,c,d)
-
-let make_letin_clause _ = List.map (out_letin_clause dummy_loc)
-
 ifdef Quotify then
+module Prelude = struct
 let fail_default_value = Qast.Int "0"
 
-ifdef Quotify then
 let out_letin_clause loc = function
   | Qast.Node ("LETTOPCLAUSE", _) -> user_err_loc (loc, "", (str "Syntax Error"))
   | Qast.Node ("LETCLAUSE", [id;c;d]) ->
       Qast.Tuple [id;c;d]
+  | _ -> anomaly "out_letin_clause"
 
-ifdef Quotify then
-let make_letin_clause loc = function
-  | Qast.List l -> Qast.List (List.map (out_letin_clause loc) l)
+let make_letin_clause _ = function
+  | Qast.List l -> Qast.List (List.map (out_letin_clause dummy_loc) l)
+  | _ -> anomaly "make_letin_clause"
+end
+else
+module Prelude = struct
+let fail_default_value = 0
+
+let out_letin_clause loc = function
+  | LETTOPCLAUSE _ -> user_err_loc (loc, "", (str "Syntax Error"))
+  | LETCLAUSE (id,c,d) -> (id,c,d)
+
+let make_letin_clause loc = List.map (out_letin_clause loc)
+end
+
+open Prelude
 
 (* Tactics grammar rules *)
 
diff --git a/parsing/g_natsyntax.ml b/parsing/g_natsyntax.ml
index 97ffba1d0d..ae36762326 100644
--- a/parsing/g_natsyntax.ml
+++ b/parsing/g_natsyntax.ml
@@ -21,8 +21,6 @@ open Coqlib
 open Termast
 open Extend
 
-exception Non_closed_number
-
 let ast_O = ast_of_ref glob_O
 let ast_S = ast_of_ref glob_S
   
@@ -55,6 +53,8 @@ let nat_of_string s dloc =
 let pat_nat_of_string s dloc = 
   pat_nat_of_int (int_of_string s) dloc
     
+exception Non_closed_number
+
 let rec int_of_nat_rec astS astO p =
   match p with
     | Node (_,"APPLIST", [b; a]) when alpha_eq(b,astS) ->
@@ -84,6 +84,8 @@ let nat_printer std_pr p =
     | Some i -> str (string_of_int i)
     | None -> pr_S (pr_external_S std_pr p)
 
+let nat_printer_0 _ _ = str "0"
+
 let _ = Esyntax.Ppprim.add ("nat_printer", nat_printer)
 
 (* Declare the primitive parser *)
@@ -104,3 +106,79 @@ let _ =
     [None, None,
      [[Gramext.Stoken ("INT", "")],
       Gramext.action pat_nat_of_string]]
+
+
+(**********************************************************************)
+(* Parsing *)
+(* For example, (nat_of_string "3") is <<(S (S (S O)))>> *)
+
+open Rawterm
+open Libnames
+open Bignat
+open Symbols
+
+let nat_of_int dloc = function
+  | POS n ->
+      if less_than (of_string "5000") n & Options.is_verbose () then begin
+	warning ("You may experiment stack overflow and segmentation fault\
+                  \nwhile parsing numbers in nat greater than 5000");
+	flush_all ()
+      end;
+      let ref_O = RRef (dloc, glob_O) in
+      let ref_S = RRef (dloc, glob_S) in
+      let rec mk_nat n =
+	if is_nonzero n then 
+	  RApp (dloc,ref_S, [mk_nat (sub_1 n)])
+	else 
+	  ref_O
+      in 
+      mk_nat n
+  | NEG n ->
+      user_err_loc (dloc, "nat_of_int",
+        str "Cannot interpret a negative number as a natural number")
+
+
+let pat_nat_of_int dloc n name = match n with
+  | POS n -> 
+      let rec mk_nat n name =
+	if is_nonzero n then 
+	  PatCstr (dloc,path_of_S,[mk_nat (sub_1 n) Anonymous],name)
+	else 
+	  PatCstr (dloc,path_of_O,[],name)
+      in 
+      mk_nat n name
+  | NEG n ->
+      user_err_loc (dloc, "pat_nat_of_int",
+        str "Cannot interpret a negative number as a natural number")
+
+let _ = 
+  Symbols.declare_numeral_interpreter "nat_scope"
+    (nat_of_int,Some pat_nat_of_int)
+
+(***********************************************************************)
+(* Printing *)
+
+exception Non_closed_number
+
+let rec int_of_nat = function
+  | Node (_,"APPLIST", [b; a]) when alpha_eq(b,ast_S) -> (int_of_nat a) + 1
+  | a when alpha_eq(a,ast_O) -> 0
+  | _ -> raise Non_closed_number
+	  
+(* Prints not p, but the SUCCESSOR of p !!!!! *)
+let nat_printer_S p =
+  try 
+    Some (int (int_of_nat p + 1))
+  with
+    Non_closed_number -> None
+
+let nat_printer_O _ =
+  Some (int 0)
+
+(* Declare the primitive printers *)
+let _ =
+  Esyntax.declare_primitive_printer "nat_printer_S" "nat_scope" nat_printer_S
+
+let _ = 
+  Esyntax.declare_primitive_printer "nat_printer_O" "nat_scope" nat_printer_O
+
diff --git a/parsing/g_prim.ml4 b/parsing/g_prim.ml4
index d279499ab4..5363be6334 100644
--- a/parsing/g_prim.ml4
+++ b/parsing/g_prim.ml4
@@ -73,7 +73,7 @@ open Q
 
 GEXTEND Gram
   GLOBAL: var ident natural metaident integer string preident ast astpat
-  astact astlist qualid reference dirpath rawident numarg;
+  astact astlist qualid reference dirpath rawident;
 
   metaident:
     [ [ s = METAIDENT -> Nmeta (loc,s) ] ]
@@ -97,9 +97,6 @@ GEXTEND Gram
     [ [ i = INT      -> local_make_posint i
       | "-"; i = INT -> local_make_negint i ] ]
   ;
-  numarg:
-    [ [ i = INT -> Num(loc, int_of_string i) ] ]
-  ;
   field:
     [ [ s = FIELD -> local_id_of_string s ] ]
   ;
@@ -121,8 +118,8 @@ GEXTEND Gram
   ;
   reference:
     [ [ id = ident; (l,id') = fields ->
-        Tacexpr.RQualid (loc, local_make_qualid (local_append l id) id')
-      | id = ident -> Tacexpr.RIdent (loc,id)
+        Coqast.RQualid (loc, local_make_qualid (local_append l id) id')
+      | id = ident -> Coqast.RIdent (loc,id)
       ] ]
   ;
   string:
diff --git a/parsing/g_rsyntax.ml b/parsing/g_rsyntax.ml
index bc2fb999f9..6c58296274 100644
--- a/parsing/g_rsyntax.ml
+++ b/parsing/g_rsyntax.ml
@@ -14,8 +14,6 @@ open Names
 open Pcoq
 open Extend
 
-exception Non_closed_number
-
 let get_r_sign loc =
   let ast_of_id id = Astterm.globalize_constr (Nvar(loc,id)) in
   ((ast_of_id (id_of_string "R0"),
@@ -23,6 +21,7 @@ let get_r_sign loc =
     ast_of_id (id_of_string "Rplus"), 
     ast_of_id (id_of_string "NRplus")))
 
+(* Parsing via Grammar *)
 let r_of_int n dloc =
   let (ast0,ast1,astp,_) = get_r_sign dloc in
   let rec mk_r n =
@@ -48,14 +47,16 @@ let _ =
 
 (** pp **)
 
+exception Non_closed_number
+
 let rec int_of_r_rec ast1 astp p =
   match p with
     | Node (_,"APPLIST", [b; a; c]) when alpha_eq(b,astp) && 
                                          alpha_eq(a,ast1) ->
-	(int_of_r_rec ast1 astp c)+1
+        (int_of_r_rec ast1 astp c)+1
     | a when alpha_eq(a,ast1) -> 1  
     | _ -> raise Non_closed_number
-	  
+          
 let int_of_r p =
   let (_,ast1,astp,_) = get_r_sign dummy_loc in
   try 
@@ -68,16 +69,117 @@ let replace_plus p =
      ope ("REXPR",[ope("APPLIST", [astnr; ast1; p])]) 
 
 let r_printer std_pr p =
- let (_,ast1,astp,_) = get_r_sign dummy_loc in
+  let (_,ast1,astp,_) = get_r_sign dummy_loc in
   match (int_of_r p) with
     | Some i -> str (string_of_int (i+1))
     | None -> std_pr (replace_plus p)
 
 let r_printer_outside std_pr p =
- let (_,ast1,astp,_) = get_r_sign dummy_loc in
+  let (_,ast1,astp,_) = get_r_sign dummy_loc in
   match (int_of_r p) with
     | Some i -> str "``" ++ str (string_of_int (i+1)) ++ str "``"
     | None -> std_pr (replace_plus p)
 
 let _ = Esyntax.Ppprim.add ("r_printer", r_printer)
 let _ = Esyntax.Ppprim.add ("r_printer_outside", r_printer_outside)
+
+(**********************************************************************)
+(* Parsing via scopes                                                 *)
+(**********************************************************************)
+
+open Libnames
+open Rawterm
+open Bignat
+
+let make_dir l = make_dirpath (List.map id_of_string (List.rev l))
+let rdefinitions = make_dir ["Coq";"Reals";"Rdefinitions"]
+
+(* TODO: temporary hack *)
+let make_path dir id = Libnames.encode_kn dir (id_of_string id)
+
+let glob_R1 = ConstRef (make_path rdefinitions "R1")
+let glob_R0 = ConstRef (make_path rdefinitions "R0")
+let glob_Ropp = ConstRef (make_path rdefinitions "Ropp")
+let glob_Rplus = ConstRef (make_path rdefinitions "Rplus")
+
+let r_of_posint dloc n =
+  if is_nonzero n then begin
+    if Options.is_verbose () & less_than (of_string "5000") n then begin
+	warning ("You may experiment stack overflow and segmentation fault\
+                  \nwhile parsing numbers in R the absolute value of which is\
+                  \ngreater than 5000");
+	flush_all ()
+      end;
+    let ref_R1 = RRef (dloc, glob_R1) in
+    let ref_Rplus = RRef (dloc, glob_Rplus) in
+    let rec r_of_strictly_pos n =
+      if is_one n then
+        ref_R1
+      else
+        RApp(dloc, ref_Rplus, [ref_R1; r_of_strictly_pos (sub_1 n)])
+    in r_of_strictly_pos n
+  end
+  else
+    RRef (dloc, glob_R0)
+
+let check_required_module loc d =
+  let d' = List.map id_of_string d in
+  let dir = make_dirpath (List.rev d') in
+  if not (Library.library_is_loaded dir) then
+    user_err_loc (loc,"z_of_int",
+    str ("Cannot interpret numbers in Z without requiring first module "
+    ^(list_last d)))
+
+let r_of_int dloc z =
+  check_required_module dloc ["Coq";"Reals";"Rsyntax"];
+  match z with
+  | NEG n -> RApp (dloc, RRef(dloc,glob_Ropp), [r_of_posint dloc n]) 
+  | POS n -> r_of_posint dloc n 
+
+let _ = Symbols.declare_numeral_interpreter "R_scope" (r_of_int,None)
+
+(***********************************************************************)
+(* Printers *)
+
+exception Non_closed_number
+
+let bignat_of_pos p =
+  let (_,one,plus,_) = get_r_sign dummy_loc in
+  let rec transl = function
+    | Node (_,"APPLIST",[p; o; a]) when alpha_eq(p,plus) & alpha_eq(o,one)
+        -> add_1(transl a)
+    | a when alpha_eq(a,one) -> Bignat.one
+    | _ -> raise Non_closed_number
+  in transl p
+	  
+let bignat_option_of_pos p =
+  try 
+    Some (bignat_of_pos p)
+  with Non_closed_number -> 
+    None
+
+let r_printer_Rplus1 p =
+  match bignat_option_of_pos p with
+    | Some n -> Some (str (Bignat.to_string (add_1 n)))
+    | None -> None
+
+let r_printer_Ropp p =
+  match bignat_option_of_pos p with
+    | Some n -> Some (str "-" ++ str (Bignat.to_string n))
+    | None -> None
+
+let r_printer_R1 _ =
+  Some (int 1)
+
+let r_printer_R0 _ =
+  Some (int 0)
+
+(* Declare pretty-printers for integers *)
+let _ =
+  Esyntax.declare_primitive_printer "r_printer_Ropp" "R_scope" (r_printer_Ropp)
+let _ =
+  Esyntax.declare_primitive_printer "r_printer_Rplus1" "R_scope" (r_printer_Rplus1)
+let _ =
+  Esyntax.declare_primitive_printer "r_printer_R1" "R_scope" (r_printer_R1)
+let _ =
+  Esyntax.declare_primitive_printer "r_printer_R0" "R_scope" r_printer_R0
diff --git a/parsing/g_zsyntax.ml b/parsing/g_zsyntax.ml
index c4e94695d7..56ded08379 100644
--- a/parsing/g_zsyntax.ml
+++ b/parsing/g_zsyntax.ml
@@ -25,89 +25,42 @@ let get_z_sign loc =
     ast_of_id (id_of_string "POS"),
     ast_of_id (id_of_string "NEG")))
 
-let int_array_of_string s =
-  let a = Array.create (String.length s) 0 in
-  for i = 0 to String.length s - 1 do
-    a.(i) <- int_of_string (String.sub s i 1)
-  done;
-  a
-    
-let string_of_int_array s =
-  String.concat "" (Array.to_list (Array.map string_of_int s))
-    
-let is_nonzero a =
-  let b = ref false in Array.iter (fun x -> b := x <> 0 || !b) a; !b
-      
-let div2_with_rest n =
-  let len = Array.length n in
-  let q = Array.create len 0 in
-  for i = 0 to len - 2 do
-    q.(i) <- q.(i) + n.(i) / 2; q.(i + 1) <- 5 * (n.(i) mod 2)
-  done;
-  q.(len - 1) <- q.(len - 1) + n.(len - 1) / 2;
-  q, n.(len - 1) mod 2
-
-let add_1 n =
-  let m = Array.copy n
-  and i = ref (Array.length n - 1) in
-  m.(!i) <- m.(!i) + 1;
-  while m.(!i) = 10 && !i > 0 do
-    m.(!i) <- 0; decr i; m.(!i) <- m.(!i) + 1
-  done;
-  if !i = 0 && m.(0) = 10 then begin 
-    m.(0) <- 0; Array.concat [[| 1 |]; m] 
-  end else 
-    m
-
-let rec mult_2 n =
-  let m = Array.copy n in
-  m.(Array.length n - 1) <- 2 * m.(Array.length n - 1);
-  for i = Array.length n - 2 downto 0 do
-    m.(i) <- 2 * m.(i);
-    if m.(i + 1) >= 10 then begin
-      m.(i + 1) <- m.(i + 1) - 10; m.(i) <- m.(i) + 1 
-    end
-  done;
-  if m.(0) >= 10 then begin 
-    m.(0) <- m.(0) - 10; Array.concat [[| 1 |]; m] 
-  end else 
-    m
-
-let pos_of_int_array astxI astxO astxH x =
+open Bignat
+
+let pos_of_bignat astxI astxO astxH x =
   let rec pos_of x =
     match div2_with_rest x with
-      | (q, 1) ->
-          if is_nonzero q then ope("APPLIST", [astxI; pos_of q]) else astxH
-      | (q, 0) -> ope("APPLIST", [astxO; pos_of q])
-      | _ -> anomaly "n mod 2 is neither 1 nor 0. Do you bielive that ?"
+      | (q, true) when is_nonzero q -> ope("APPLIST", [astxI; pos_of q])
+      | (q, false) -> ope("APPLIST", [astxO; pos_of q])
+      | (_, true) -> astxH
   in 
   pos_of x
     
 let z_of_string pos_or_neg s dloc = 
   let ((astxI,astxO,astxH),(astZERO,astPOS,astNEG)) = get_z_sign dloc in
-  let v = int_array_of_string s in
+  let v = Bignat.of_string s in
   if is_nonzero v then
     if pos_or_neg then
-      ope("APPLIST",[astPOS; pos_of_int_array astxI astxO astxH v])
+      ope("APPLIST",[astPOS; pos_of_bignat astxI astxO astxH v])
     else 
-      ope("APPLIST",[astNEG; pos_of_int_array astxI astxO astxH v])
+      ope("APPLIST",[astNEG; pos_of_bignat astxI astxO astxH v])
   else 
     astZERO
       
 exception Non_closed_number
 
-let rec int_array_of_pos c1 c2 c3 p =
+let rec bignat_of_pos c1 c2 c3 p =
   match p with
     | Node (_,"APPLIST", [b; a]) when alpha_eq(b,c1) ->
-        mult_2 (int_array_of_pos c1 c2 c3 a)
+        mult_2 (bignat_of_pos c1 c2 c3 a)
     | Node (_,"APPLIST", [b; a]) when alpha_eq(b,c2) ->
-        add_1 (mult_2 (int_array_of_pos c1 c2 c3 a))
-    | a when alpha_eq(a,c3) -> [| 1 |]
+        add_1 (mult_2 (bignat_of_pos c1 c2 c3 a))
+    | a when alpha_eq(a,c3) -> Bignat.one
     | _ -> raise Non_closed_number
 	  
-let int_array_option_of_pos astxI astxO astxH p =
+let bignat_option_of_pos astxI astxO astxH p =
   try 
-    Some (int_array_of_pos astxO astxI astxH p)
+    Some (bignat_of_pos astxO astxI astxH p)
   with Non_closed_number -> 
     None
 
@@ -116,35 +69,37 @@ let pr_neg a = hov 0 (str "NEG" ++ brk (1,1) ++ a)
 
 let inside_printer posneg std_pr p =
   let ((astxI,astxO,astxH),_) = get_z_sign dummy_loc in
-  match (int_array_option_of_pos astxI astxO astxH p) with
+  match (bignat_option_of_pos astxI astxO astxH p) with
     | Some n -> 
 	if posneg then 
-	  (str (string_of_int_array n))
+	  (str (Bignat.to_string n))
 	else 
-	  (str "(-" ++ str (string_of_int_array n) ++ str ")")
+	  (str "(-" ++ str (Bignat.to_string n) ++ str ")")
     | None -> 
 	let pr = if posneg then pr_pos else pr_neg in
 	str "(" ++ pr (std_pr (ope("ZEXPR",[p]))) ++ str ")"
 
+let outside_zero_printer std_pr p = str "`0`"
+
 let outside_printer posneg std_pr p =
   let ((astxI,astxO,astxH),_) = get_z_sign dummy_loc in
-  match (int_array_option_of_pos astxI astxO astxH p) with
+  match (bignat_option_of_pos astxI astxO astxH p) with
     | Some n -> 
 	if posneg then 
-	  (str "`" ++ str (string_of_int_array n) ++ str "`")
+	  (str "`" ++ str (Bignat.to_string n) ++ str "`")
 	else 
-	  (str "`-" ++ str (string_of_int_array n) ++ str "`")
+	  (str "`-" ++ str (Bignat.to_string n) ++ str "`")
       | None -> 
 	  let pr = if posneg then pr_pos else pr_neg in
 	  str "(" ++ pr (std_pr p) ++ str ")"
 
-(* Declare pretty-printers for integers *)
+(* For printing with Syntax and without the scope mechanism *)
 let _ = Esyntax.Ppprim.add ("positive_printer", (outside_printer true))
 let _ = Esyntax.Ppprim.add ("negative_printer", (outside_printer false))
 let _ = Esyntax.Ppprim.add ("positive_printer_inside", (inside_printer true))
 let _ = Esyntax.Ppprim.add ("negative_printer_inside", (inside_printer false))
 
-(* Declare the primitive parser *)
+(* Declare the primitive parser with Grammar and without the scope mechanism *)
 open Pcoq
 
 let number = create_constr_entry (get_univ "znatural") "number" 
@@ -163,3 +118,104 @@ let _ =
      [[Gramext.Stoken ("INT", "")],
       Gramext.action (z_of_string false)]]
 
+(**********************************************************************)
+(* Parsing via scopes                                                 *)
+(**********************************************************************)
+
+open Libnames
+open Rawterm
+let make_dir l = make_dirpath (List.map id_of_string (List.rev l))
+let fast_integer_module = make_dir ["Coq";"ZArith";"fast_integer"]
+
+(* TODO: temporary hack *)
+let make_path dir id = Libnames.encode_kn dir id
+
+let z_path = make_path fast_integer_module (id_of_string "Z")
+let glob_z = IndRef (z_path,0)
+let glob_ZERO = ConstructRef ((z_path,0),1)
+let glob_POS = ConstructRef ((z_path,0),2)
+let glob_NEG = ConstructRef ((z_path,0),3)
+
+let positive_path = make_path fast_integer_module (id_of_string "positive")
+let glob_xI = ConstructRef ((positive_path,0),1)
+let glob_xO = ConstructRef ((positive_path,0),2)
+let glob_xH = ConstructRef ((positive_path,0),3)
+
+let pos_of_bignat dloc x =
+  let ref_xI = RRef (dloc, glob_xI) in
+  let ref_xH = RRef (dloc, glob_xH) in
+  let ref_xO = RRef (dloc, glob_xO) in
+  let rec pos_of x =
+    match div2_with_rest x with
+      | (q,false) -> RApp (dloc, ref_xO,[pos_of q])
+      | (q,true) when is_nonzero q -> RApp (dloc,ref_xI,[pos_of q])
+      | (q,true) -> ref_xH
+  in 
+  pos_of x
+
+let z_of_string2 dloc pos_or_neg n = 
+  if is_nonzero n then
+    let sgn = if pos_or_neg then glob_POS else glob_NEG in
+    RApp(dloc, RRef (dloc,sgn), [pos_of_bignat dloc n])
+  else 
+    RRef (dloc, glob_ZERO)
+
+let check_required_module loc d =
+  let d' = List.map id_of_string d in
+  let dir = make_dirpath (List.rev d') in
+  if not (Library.library_is_loaded dir) then
+    user_err_loc (loc,"z_of_int",
+    str ("Cannot interpret numbers in Z without requiring first module "
+    ^(list_last d)))
+
+let z_of_int dloc z =
+  check_required_module dloc ["Coq";"ZArith";"Zsyntax"];
+  match z with
+  | POS n -> z_of_string2 dloc true n 
+  | NEG n -> z_of_string2 dloc false n 
+
+let _ = Symbols.declare_numeral_interpreter "Z_scope" (z_of_int,None)
+
+(***********************************************************************)
+(* Printers *)
+
+exception Non_closed_number
+
+let bignat_of_pos p =
+  let ((astxI,astxO,astxH),_) = get_z_sign dummy_loc in
+  let c1 = astxO in
+  let c2 = astxI in
+  let c3 = astxH in
+  let rec transl = function
+    | Node (_,"APPLIST",[b; a]) when alpha_eq(b,c1) -> mult_2(transl a)
+    | Node (_,"APPLIST",[b; a]) when alpha_eq(b,c2) -> add_1(mult_2(transl a))
+    | a when alpha_eq(a,c3) -> Bignat.one
+    | _ -> raise Non_closed_number
+  in transl p
+	  
+let bignat_option_of_pos p =
+  try 
+    Some (bignat_of_pos p)
+  with Non_closed_number -> 
+    None
+
+let z_printer posneg p =
+  match bignat_option_of_pos p with
+    | Some n -> 
+	if posneg then 
+	  Some (str (Bignat.to_string n))
+	else 
+	  Some (str "-" ++ str (Bignat.to_string n))
+    | None -> None
+
+let z_printer_ZERO _ =
+  Some (int 0)
+
+(* Declare pretty-printers for integers *)
+open Esyntax
+let _ =
+  declare_primitive_printer "z_printer_POS" "Z_scope" (z_printer true)
+let _ =
+  declare_primitive_printer "z_printer_NEG" "Z_scope" (z_printer false)
+let _ =
+  declare_primitive_printer "z_printer_ZERO" "Z_scope" z_printer_ZERO
diff --git a/parsing/symbols.ml b/parsing/symbols.ml
new file mode 100644
index 0000000000..e13fd3df4b
--- /dev/null
+++ b/parsing/symbols.ml
@@ -0,0 +1,265 @@
+open Util
+open Pp
+open Names
+open Nametab
+open Summary
+open Rawterm
+open Bignat
+
+(* A scope is a set of notations; it includes
+
+  - a set of ML interpreters/parsers for positive (e.g. 0, 1, 15, ...) and
+    negative numbers (e.g. -0, -2, -13, ...). These interpreters may
+    fail if a number has no interpretation in the scope (e.g. there is
+    no interpretation for negative numbers in [nat]); interpreters both for
+    terms and patterns can be set; these interpreters are in permanent table
+    [numeral_interpreter_tab]
+  - a set of ML printers for expressions denoting numbers parsable in 
+    this scope (permanently declared in [Esyntax.primitive_printer_tab])
+  - a set of interpretations for infix (more generally distfix) notations
+  - an optional pair of delimiters which, when occurring in a syntactic
+    expression, set this scope to be the current scope
+*)
+
+let pr_bigint = function
+  | POS n -> str (Bignat.to_string n)
+  | NEG n -> str "-" ++ str (Bignat.to_string n)
+
+(**********************************************************************)
+(* Scope of symbols *)
+
+type notation = string
+type scope_name = string
+type delimiters = string * string
+type scope = {
+  notations: rawconstr Stringmap.t;
+  delimiters: delimiters option
+}
+type scopes = scope_name list
+
+(* Scopes table: scope_name -> symbol_interpretation *)
+let scope_map = ref Stringmap.empty
+
+let empty_scope = {
+  notations = Stringmap.empty;
+  delimiters = None
+}
+
+let default_scope = "core_scope"
+
+let _ = Stringmap.add default_scope empty_scope !scope_map
+
+let scope_stack = ref [default_scope]
+
+let current_scopes () = !scope_stack
+
+(* TODO: push nat_scope, z_scope, ... in scopes summary *)
+
+(**********************************************************************)
+(* Interpreting numbers (not in summary because functional objects)   *)
+
+type numeral_interpreter_name = string
+type numeral_interpreter =
+    (loc -> bigint -> rawconstr)
+    * (loc -> bigint -> name -> cases_pattern) option
+
+let numeral_interpreter_tab =
+  (Hashtbl.create 17 : (numeral_interpreter_name,numeral_interpreter)Hashtbl.t)
+
+let declare_numeral_interpreter sc t =
+  Hashtbl.add numeral_interpreter_tab sc t
+
+let lookup_numeral_interpreter s =
+  try 
+    Hashtbl.find numeral_interpreter_tab s
+  with Not_found -> 
+    error ("No interpretation for numerals in scope "^s)
+
+(* For loading without opening *)
+let declare_scope scope =
+  try let _ = Stringmap.find scope !scope_map in ()
+  with Not_found -> scope_map := Stringmap.add scope empty_scope !scope_map
+
+let declare_delimiters scope dlm =
+  let sc =
+    try Stringmap.find scope !scope_map
+    with Not_found -> empty_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   
+
+(* The mapping between notations and production *)
+
+let declare_notation nt c scope =
+  let sc =
+    try Stringmap.find scope !scope_map
+    with Not_found -> empty_scope
+  in
+  if Stringmap.mem nt sc.notations && Options.is_verbose () then
+    warning ("Notation "^nt^" is already used in scope "^scope);
+  let sc = { sc with notations = Stringmap.add nt c sc.notations } in
+  scope_map := Stringmap.add scope sc !scope_map
+
+open Coqast
+
+let rec subst_meta_rawconstr subst = function
+  | RMeta (_,n) -> List.nth subst (n-1)
+  | t -> map_rawconstr (subst_meta_rawconstr subst) t
+
+let rec find_interpretation f = function
+  | scope::scopes ->
+      (try f (Stringmap.find scope !scope_map)
+       with Not_found -> find_interpretation f scopes)
+  | [] -> raise Not_found
+
+let rec interp_notation ntn scopes args =
+  let f scope =
+    let c = Stringmap.find ntn scope.notations in
+    subst_meta_rawconstr args c in
+  try find_interpretation f scopes
+  with Not_found -> anomaly ("Unknown interpretation for notation "^ntn)
+
+let find_notation_with_delimiters scope =
+  match (Stringmap.find scope !scope_map).delimiters with
+    | Some dlm -> Some (Some dlm)
+    | None -> None
+
+let rec find_notation_without_delimiters pat_scope pat = function
+  | scope::scopes ->
+      (* Is the expected printer attached to the most recently open scope? *)
+      if scope = pat_scope then
+	Some None
+      else
+	(* If the most recently open scope has a printer for this pattern
+    	   but not the expected one then we need delimiters *)
+	if Stringmap.mem pat (Stringmap.find scope !scope_map).notations then
+	  find_notation_with_delimiters pat_scope
+	else
+	  find_notation_without_delimiters pat_scope pat scopes
+  | [] ->
+      find_notation_with_delimiters pat_scope
+
+let find_notation pat_scope pat scopes =
+  match 
+    find_notation_without_delimiters pat_scope pat scopes
+  with
+    | None -> None
+    | Some None -> Some (None,scopes)
+    | Some x -> Some (x,pat_scope::scopes)
+
+let exists_notation_in_scope scope ntn =
+  try Stringmap.mem ntn (Stringmap.find scope !scope_map).notations
+  with Not_found -> false
+
+let exists_notation nt =
+  Stringmap.fold (fun scn sc b -> Stringmap.mem nt sc.notations or b)
+    !scope_map false 
+
+(* TO DO
+let print_scope sc =
+  try
+    let sc = Stringmap.find scope !scope_map in
+    Stringmap.fold (fun ntn c s -> s ++ str ntn ++ Printer.pr_rawterm c)
+      sc.notations in
+  with Not_found -> str "Unknown scope"
+*)
+
+(* We have to print delimiters; look for the more recent defined one *)
+(* Do we need to print delimiters? To know it, we look for a numeral *)
+(* printer available in the current stack of scopes *)
+let find_numeral_with_delimiters scope =
+  match (Stringmap.find scope !scope_map).delimiters with
+    | Some dlm -> Some (Some dlm)
+    | None -> None
+
+let rec find_numeral_without_delimiters printer_scope = function
+  | scope :: scopes -> 
+      (* Is the expected printer attached to the most recently open scope? *)
+      if scope = printer_scope then
+	Some None
+      else
+	(* If the most recently open scope has a printer for numerals
+    	   but not the expected one then we need delimiters *)
+	if not (Hashtbl.mem numeral_interpreter_tab scope) then
+	  find_numeral_without_delimiters printer_scope scopes
+	else
+	  find_numeral_with_delimiters printer_scope
+  | [] ->
+      (* Can we switch to [scope]? Yes if it has defined delimiters *)
+      find_numeral_with_delimiters printer_scope
+
+let find_numeral_printer printer_scope scopes =
+  match 
+    find_numeral_without_delimiters printer_scope scopes
+  with
+    | None -> None
+    | Some None -> Some (None,scopes)
+    | Some x -> Some (x,printer_scope::scopes)
+
+(* This is the map associating the scope a numeral printer belongs to *)
+(*
+let numeral_printer_map = ref (Stringmap.empty : scope_name Stringmap.t)
+*)
+
+let rec interp_numeral loc n = function
+  | scope :: scopes ->
+      (try fst (lookup_numeral_interpreter scope) loc n
+       with Not_found -> interp_numeral loc n scopes)
+  | [] ->
+      user_err_loc (loc,"interp_numeral",
+      str "No interpretation for numeral " ++ pr_bigint n)
+
+let rec interp_numeral_as_pattern loc n name = function
+  | scope :: scopes ->
+      (try 
+	match snd (lookup_numeral_interpreter scope) with
+	  | None -> raise Not_found
+	  | Some g -> g loc n name
+	with Not_found -> interp_numeral_as_pattern loc n name scopes)
+  | [] ->
+      user_err_loc (loc,"interp_numeral_as_pattern",
+      str "No interpretation for numeral " ++ pr_bigint n)
+
+(* Exportation of scopes *)
+let cache_scope (_,sc) =
+  if Stringmap.mem sc !scope_map then
+    scope_stack := sc :: !scope_stack
+  else
+    error ("Unknown scope: "^sc)
+
+let subst_scope (_,subst,sc) = sc
+
+open Libobject
+
+let (inScope,outScope) = 
+  declare_object {(default_object "SCOPE") with
+      cache_function = cache_scope;
+      open_function = (fun i o -> if i=1 then cache_scope o);
+      subst_function = subst_scope;
+      classify_function = (fun (_,o) -> Substitute o);
+      export_function = (fun x -> Some x) }
+
+let open_scope sc = Lib.add_anonymous_leaf (inScope sc)
+
+(* Synchronisation with reset *)
+
+let freeze () = (!scope_map, !scope_stack)
+
+let unfreeze (scm,scs) =
+  scope_map := scm;
+  scope_stack := scs
+
+let init () = ()
+(*
+  scope_map := Strinmap.empty;
+  scope_stack := Stringmap.empty
+*)
+
+let _ = 
+  declare_summary "symbols"
+    { freeze_function = freeze;
+      unfreeze_function = unfreeze;
+      init_function = init;
+      survive_section = false }
diff --git a/parsing/symbols.mli b/parsing/symbols.mli
new file mode 100644
index 0000000000..c0d8eea294
--- /dev/null
+++ b/parsing/symbols.mli
@@ -0,0 +1,48 @@
+open Names
+open Util
+open Nametab
+open Rawterm
+open Bignat
+
+(* A numeral interpreter is the pair of an interpreter for _integer_
+   numbers in terms and an optional interpreter in pattern, if
+   negative numbers are not supported, the interpreter must fail with
+   an appropriate error message *)
+
+type numeral_interpreter_name = string
+type numeral_interpreter =
+    (loc -> bigint -> rawconstr)
+    * (loc -> bigint -> name -> cases_pattern) option
+
+(* A scope is a set of interpreters for symbols + optional
+   interpreter and printers for integers + optional delimiters *)
+
+type scope_name = string
+type delimiters = string * string
+type scope
+type scopes = scope_name list
+
+val default_scope : scope_name
+val current_scopes : unit -> scopes
+val open_scope : scope_name -> unit
+val declare_scope : scope_name -> unit
+
+(* Declare delimiters for printing *)
+val declare_delimiters : scope_name -> delimiters -> unit
+
+(* Declare, interpret, and look for a printer for numeral *)
+val declare_numeral_interpreter :
+  numeral_interpreter_name -> numeral_interpreter -> unit
+val interp_numeral : loc -> bigint -> scopes -> rawconstr
+val interp_numeral_as_pattern: loc -> bigint -> name -> scopes -> cases_pattern
+val find_numeral_printer : string -> scopes ->
+  (delimiters option * scopes) option
+
+(* Declare, interpret, and look for a printer for symbolic notations *)
+type notation = string
+val declare_notation : notation -> rawconstr -> scope_name -> unit
+val interp_notation : notation -> scopes -> rawconstr  list -> rawconstr
+val find_notation : scope_name -> notation -> scopes -> 
+  (delimiters option * scopes) option
+val exists_notation_in_scope : scope_name -> notation -> bool
+val exists_notation : notation -> bool