Ajout d'un mécanisme d'interprétation et d'affichage pour les littéraux de chaîne de caractères tel que "foo"

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

11 files changed, 172 insertions, 119 deletions

diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml
index f0e9c120bc..bd9e1f7f31 100644
--- a/contrib/interface/xlate.ml
+++ b/contrib/interface/xlate.ml
@@ -264,9 +264,10 @@ let rec xlate_match_pattern =
     | CPatOr (_,l) -> xlate_error "CPatOr: TODO"
     | CPatDelimiters(_, key, p) -> 
 	CT_pattern_delimitors(CT_num_type key, xlate_match_pattern p)
-    | CPatNumeral(_,n) ->
+    | CPatPrim (_,Numeral n) ->
  	CT_coerce_NUM_to_MATCH_PATTERN
 	  (CT_int_encapsulator(Bigint.to_string n))
+    | CPatPrim (_,String _) -> xlate_error "CPatPrim (String): TODO"
     | CPatNotation(_, s, l) -> 
 	CT_pattern_notation(CT_string s,
 			    CT_match_pattern_list(List.map xlate_match_pattern l))
@@ -388,8 +389,9 @@ and (xlate_formula:Topconstr.constr_expr -> Ascent.ct_FORMULA) = function
 
    | CSort(_, s) -> CT_coerce_SORT_TYPE_to_FORMULA(xlate_sort s)
    | CNotation(_, s, l) -> notation_to_formula s (List.map xlate_formula l)
-   | CNumeral(_, i) -> 
+   | CPrim (_, Numeral i) -> 
        CT_coerce_NUM_to_FORMULA(CT_int_encapsulator(Bigint.to_string i))
+   | CPrim (_, String _) -> xlate_error "CPrim (String): TODO"
    | CHole _ -> CT_existvarc 
 (* I assume CDynamic has been inserted to make free form extension of
    the language possible, but this would go agains the logic of pcoq anyway. *)
diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 5b448efef6..a8a6b862e8 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -54,7 +54,7 @@ let print_coercions = ref false
 (* This forces printing universe names of Type{.} *)
 let print_universes = ref false
 
-(* This suppresses printing of numeral and symbols *)
+(* This suppresses printing of primitive tokens (e.g. numeral) and symbols *)
 let print_no_symbol = ref false
 
 (* This governs printing of projections using the dot notation symbols *)
@@ -131,7 +131,7 @@ let rec check_same_pattern p1 p2 =
     | CPatCstr(_,c1,a1), CPatCstr(_,c2,a2) when c1=c2 ->
         List.iter2 check_same_pattern a1 a2
     | CPatAtom(_,r1), CPatAtom(_,r2) when r1=r2 -> ()
-    | CPatNumeral(_,i1), CPatNumeral(_,i2) when i1=i2 -> ()
+    | CPatPrim(_,i1), CPatPrim(_,i2) when i1=i2 -> ()
     | CPatDelimiters(_,s1,e1), CPatDelimiters(_,s2,e2) when s1=s2 ->
         check_same_pattern e1 e2
     | _ -> failwith "not same pattern"
@@ -191,7 +191,7 @@ let rec check_same_type ty1 ty2 =
       check_same_type b1 b2
   | CNotation(_,n1,e1), CNotation(_,n2,e2) when n1=n2 ->
       List.iter2 check_same_type e1 e2
-  | CNumeral(_,i1), CNumeral(_,i2) when i1=i2 -> ()
+  | CPrim(_,i1), CPrim(_,i2) when i1=i2 -> ()
   | CDelimiters(_,s1,e1), CDelimiters(_,s2,e2) when s1=s2 ->
       check_same_type e1 e2
   | _ when ty1=ty2 -> ()
@@ -330,7 +330,7 @@ let make_notation loc ntn l =
   then expand_curly_brackets (fun n l -> CNotation (loc,n,l)) ntn l
   else match ntn,l with
     (* Special case to avoid writing "- 3" for e.g. (Zopp 3) *)
-    | "- _", [CNumeral(_,p)] when Bigint.is_strictly_pos p ->
+    | "- _", [CPrim(_,Numeral p)] when Bigint.is_strictly_pos p ->
         CNotation (loc,ntn,[CNotation(loc,"( _ )",l)])
     | _ -> CNotation (loc,ntn,l)
 
@@ -339,7 +339,7 @@ let make_pat_notation loc ntn l =
   then expand_curly_brackets (fun n l -> CPatNotation (loc,n,l)) ntn l
   else match ntn,l with
     (* Special case to avoid writing "- 3" for e.g. (Zopp 3) *)
-    | "- _", [CPatNumeral(_,p)] when Bigint.is_strictly_pos p ->
+    | "- _", [CPatPrim (_,Numeral p)] when Bigint.is_strictly_pos p ->
         CPatNotation (loc,ntn,[CPatNotation(loc,"( _ )",l)])
     | _ -> CPatNotation (loc,ntn,l)
 
@@ -385,17 +385,17 @@ let match_aconstr_cases_pattern c (metas_scl,pat) =
 let rec extern_cases_pattern_in_scope scopes vars pat =
   try 
     if !Options.raw_print or !print_no_symbol then raise No_match;
-    let (sc,n) = Notation.uninterp_cases_numeral pat in
-    match Notation.availability_of_numeral sc (make_current_scopes scopes) with
+    let (sc,p) = uninterp_prim_token_cases_pattern pat in
+    match availability_of_prim_token sc (make_current_scopes scopes) with
     | None -> raise No_match
     | Some key ->
         let loc = pattern_loc pat in
-        insert_pat_delimiters (CPatNumeral (loc,n)) key
+        insert_pat_delimiters (CPatPrim (loc,p)) key
   with No_match ->
   try 
     if !Options.raw_print or !print_no_symbol then raise No_match;
     extern_symbol_pattern scopes vars pat
-      (Notation.uninterp_cases_pattern_notations pat)
+      (uninterp_cases_pattern_notations pat)
   with No_match ->
   match pat with
   | PatVar (loc,Name id) -> CPatAtom (loc,Some (Ident (loc,id)))
@@ -424,7 +424,7 @@ and extern_symbol_pattern (tmp_scope,scopes as allscopes) vars t = function
         match keyrule with
           | NotationRule (sc,ntn) ->
 	      let scopes' = make_current_scopes (tmp_scope, scopes) in
-	      (match Notation.availability_of_notation (sc,ntn) scopes' with
+	      (match availability_of_notation (sc,ntn) scopes' with
                   (* Uninterpretation is not allowed in current context *)
               | None -> raise No_match
                   (* Uninterpretation is allowed in current context *)
@@ -588,15 +588,14 @@ let rec share_fix_binders n rbl ty def =
 let rec extern inctx scopes vars r =
   try 
     if !Options.raw_print or !print_no_symbol then raise No_match;
-    extern_numeral (Rawterm.loc_of_rawconstr r)
-      scopes (Notation.uninterp_numeral r)
+    extern_prim_token (loc_of_rawconstr r) scopes (uninterp_prim_token r)
   with No_match ->
 
   let r = remove_coercions inctx r in
 
   try 
     if !Options.raw_print or !print_no_symbol then raise No_match;
-    extern_symbol scopes vars r (Notation.uninterp_notations r)
+    extern_symbol scopes vars r (uninterp_notations r)
   with No_match -> match r with
   | RRef (loc,ref) ->
       extern_global loc (implicits_of_global ref)
@@ -611,7 +610,7 @@ let rec extern inctx scopes vars r =
   | RApp (loc,f,args) ->
       (match f with
 	 | RRef (rloc,ref) ->
-	     let subscopes = Notation.find_arguments_scope ref in
+	     let subscopes = find_arguments_scope ref in
 	     let args =
 	       extern_args (extern true) (snd scopes) vars args subscopes in
 	     extern_app loc inctx (implicits_of_global ref)
@@ -766,10 +765,10 @@ and extern_eqn inctx scopes vars (loc,ids,pl,c) =
   (loc,List.map (extern_cases_pattern_in_scope scopes vars) pl,
    extern inctx scopes vars c)
 
-and extern_numeral loc scopes (sc,n) =
-  match Notation.availability_of_numeral sc (make_current_scopes scopes) with
-    | None -> raise No_match
-    | Some key -> insert_delimiters (CNumeral (loc,n)) key
+and extern_prim_token loc scopes (sc,p) =
+  match availability_of_prim_token sc (make_current_scopes scopes) with
+  | None -> raise No_match
+  | Some key -> insert_delimiters (CPrim (loc,p)) key
 
 and extern_symbol (tmp_scope,scopes as allscopes) vars t = function
   | [] -> raise No_match
@@ -789,7 +788,7 @@ and extern_symbol (tmp_scope,scopes as allscopes) vars t = function
           match keyrule with
           | NotationRule (sc,ntn) ->
 	      let scopes' = make_current_scopes (tmp_scope, scopes) in
-	      (match Notation.availability_of_notation (sc,ntn) scopes' with
+	      (match availability_of_notation (sc,ntn) scopes' with
                   (* Uninterpretation is not allowed in current context *)
               | None -> raise No_match
                   (* Uninterpretation is allowed in current context *)
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index e81295214a..c7af2a5f33 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -558,11 +558,12 @@ let rec intern_cases_pattern scopes (ids,subst as aliases) tmp_scope = function
       let pl' = List.map (fun (subst,pl) ->
         (subst, PatCstr (loc,c,pl0@pl,alias_of aliases))) pll in
       ids',pl'
-  | CPatNotation (loc,"- _",[CPatNumeral(_,p)]) when Bigint.is_strictly_pos p->
+  | CPatNotation (loc,"- _",[CPatPrim(_,Numeral p)]) 
+      when Bigint.is_strictly_pos p->
       let scopes = option_cons tmp_scope scopes in
-      (ids,
-      [subst, Notation.interp_numeral_as_pattern loc (Bigint.neg p)
-        (alias_of aliases) scopes])
+      let np = Numeral (Bigint.neg p) in
+      let a = alias_of aliases in
+      (ids, [subst, Notation.interp_prim_token_cases_pattern loc np a scopes])
   | CPatNotation (_,"( _ )",[a]) ->
       intern_cases_pattern scopes aliases tmp_scope a
   | CPatNotation (loc, ntn, args) ->
@@ -572,10 +573,10 @@ let rec intern_cases_pattern scopes (ids,subst as aliases) tmp_scope = function
       if !dump then dump_notation_location (patntn_loc loc args ntn) ntn df;
       let subst = List.map2 (fun (id,scl) a -> (id,(a,scl))) ids args in
       subst_cases_pattern loc aliases intern_cases_pattern subst scopes c
-  | CPatNumeral (loc, n) ->
+  | CPatPrim (loc, p) ->
       let scopes = option_cons tmp_scope scopes in
-      (ids,[subst,
-       Notation.interp_numeral_as_pattern loc n (alias_of aliases) scopes])
+      let a = alias_of aliases in
+      (ids,[subst, Notation.interp_prim_token_cases_pattern loc p a scopes])
   | CPatDelimiters (loc, key, e) ->
       intern_cases_pattern (find_delimiters_scope loc key::scopes)
         aliases None e
@@ -836,15 +837,17 @@ let internalise sigma env allow_soapp lvar c =
     | CLetIn (loc,(_,na),c1,c2) ->
 	RLetIn (loc, na, intern (reset_tmp_scope env) c1,
           intern (push_name_env lvar env na) c2)
-    | CNotation (loc,"- _",[CNumeral(_,p)]) when Bigint.is_strictly_pos p ->
+    | CNotation (loc,"- _",[CPrim (_,Numeral p)])
+	when Bigint.is_strictly_pos p ->
         let scopes = option_cons tmp_scope scopes in
-        Notation.interp_numeral loc (Bigint.neg p) scopes
+	let np = Numeral (Bigint.neg p) in
+        Notation.interp_prim_token loc np scopes
     | CNotation (_,"( _ )",[a]) -> intern env a
     | CNotation (loc,ntn,args) ->
         intern_notation intern env loc ntn args
-    | CNumeral (loc, n) ->
+    | CPrim (loc, p) ->
 	let scopes = option_cons tmp_scope scopes in
-	Notation.interp_numeral loc n scopes
+	Notation.interp_prim_token loc p scopes
     | CDelimiters (loc, key, e) ->
 	intern (ids,None,find_delimiters_scope loc key::scopes) e
     | CAppExpl (loc, (isproj,ref), args) ->
diff --git a/interp/notation.ml b/interp/notation.ml
index 570981affa..204dc0f4a7 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -168,7 +168,7 @@ type key =
 
 (* Scopes table : interpretation -> scope_name *)
 let notations_key_table = ref Gmapl.empty
-let numeral_key_table = Hashtbl.create 7
+let prim_token_key_table = Hashtbl.create 7
 
 let rawconstr_key = function
   | RApp (_,RRef (_,ref),_) -> RefKey ref
@@ -192,41 +192,65 @@ let pattern_key = function
 (**********************************************************************)
 (* Interpreting numbers (not in summary because functional objects)   *)
 
-type num_interpreter =
-    (loc -> bigint -> rawconstr)
-    * (loc -> bigint -> name -> cases_pattern) option
+type required_module = global_reference * string list 
 
-type num_uninterpreter =
-    rawconstr list * (rawconstr -> bigint option)
-    * (cases_pattern -> bigint option) option
+type 'a prim_token_interpreter =
+    (loc -> 'a -> rawconstr) * (loc -> 'a -> name -> cases_pattern) option
 
-type required_module = global_reference * string list 
+type 'a prim_token_uninterpreter =
+    rawconstr list * (rawconstr -> 'a option)
+    * (cases_pattern -> 'a option) option
 
-let numeral_interpreter_tab =
-  (Hashtbl.create 7 : (scope_name,required_module*num_interpreter) Hashtbl.t)
+type internal_prim_token_interpreter =
+    loc -> prim_token -> 
+      required_module * ((unit -> rawconstr) * (name -> cases_pattern) option)
 
-let declare_numeral_interpreter sc dir interp (patl,uninterp,uninterpc) =
+let prim_token_interpreter_tab =
+  (Hashtbl.create 7 : (scope_name, internal_prim_token_interpreter) Hashtbl.t)
+
+let add_prim_token_interpreter sc interp =
+  try 
+    let cont = Hashtbl.find prim_token_interpreter_tab sc in
+    Hashtbl.replace prim_token_interpreter_tab sc (interp cont)
+  with Not_found ->
+    let cont = (fun _loc _p -> raise Not_found) in
+    Hashtbl.add prim_token_interpreter_tab sc (interp cont)
+
+let declare_prim_token_interpreter sc interp (patl,uninterp,uninterpc) =
   declare_scope sc;
-  Hashtbl.add numeral_interpreter_tab sc (dir,interp);
+  add_prim_token_interpreter sc interp;
   List.iter
-    (fun pat -> Hashtbl.add numeral_key_table (rawconstr_key pat)
+    (fun pat -> Hashtbl.add prim_token_key_table (rawconstr_key pat)
       (sc,uninterp,uninterpc))
     patl
 
+let mkNumeral n = Numeral n
+let mkString s = String s
+
+let delay dir (int,intc) loc x =
+  (dir, ((fun () -> int loc x), option_app (fun i -> i loc x) intc))
+
+let declare_numeral_interpreter sc dir interp (patl,uninterp,uninterpc) =
+  declare_prim_token_interpreter sc
+    (fun cont loc -> function Numeral n-> delay dir interp loc n | p -> cont loc p)
+    (patl,
+     (fun r -> option_app mkNumeral (uninterp r)),
+     option_app (fun u pc -> option_app mkNumeral (u pc)) uninterpc)
+
+let declare_string_interpreter sc dir interp (patl,uninterp,uninterpc) =
+  declare_prim_token_interpreter sc
+    (fun cont loc -> function String s -> delay dir interp loc s | p -> cont loc p)
+    (patl,
+     (fun r -> option_app mkString (uninterp r)),
+     option_app (fun u -> fun pc -> option_app mkString (u pc)) uninterpc)
+
 let check_required_module loc sc (ref,d) =
   try let _ = sp_of_global ref in ()
   with Not_found ->
-    user_err_loc (loc,"numeral_interpreter",
+    user_err_loc (loc,"prim_token_interpreter",
     str ("Cannot interpret numbers in "^sc^" without requiring first module "
     ^(list_last d)))
 
-let lookup_numeral_interpreter loc = function
-  | Scope sc ->
-      let (dir,interpreter) = Hashtbl.find numeral_interpreter_tab sc in
-      check_required_module loc sc dir;
-      interpreter
-  | SingleNotation _ -> raise Not_found
-
 (* Look if some notation or numeral printer in [scope] can be used in
    the scope stack [scopes], and if yes, using delimiters or not *)
 
@@ -314,35 +338,42 @@ let availability_of_notation (ntn_scope,ntn) scopes =
     Stringmap.mem ntn (Stringmap.find scope !scope_map).notations in
   find_without_delimiters f (ntn_scope,Some ntn) scopes
 
-let rec interp_numeral_gen loc f n = function
-  | scope :: scopes ->
-      (try f (lookup_numeral_interpreter loc scope)
-       with Not_found -> interp_numeral_gen loc f n scopes)
+let rec interp_prim_token_gen loc f p = function
+  | SingleNotation _ :: scopes -> interp_prim_token_gen loc f p scopes
+  | Scope sc :: scopes ->
+      (try 
+	let dir,interp = Hashtbl.find prim_token_interpreter_tab sc loc p in
+	check_required_module loc sc dir;
+	f interp
+       with Not_found -> 
+	 interp_prim_token_gen loc f p scopes)
   | [] ->
-      user_err_loc (loc,"interp_numeral",
-      str "No interpretation for numeral " ++ pr_bigint n)
+      user_err_loc (loc,"interp_prim_token",
+      (match p with
+	| Numeral n -> str "No interpretation for numeral " ++ pr_bigint n
+	| String s -> str "No interpretation for string " ++ qs s))
+
+let push_scopes = List.fold_right push_scope
 
-let interp_numeral loc n scopes =
-  interp_numeral_gen loc (fun x -> fst x loc n) n
-    (List.fold_right push_scope scopes !scope_stack)
+let interp_prim_token loc p scopes =
+  let f x = fst x () in
+  interp_prim_token_gen loc f p (push_scopes scopes !scope_stack)
 
-let interp_numeral_as_pattern loc n name scopes =
-  let f x = match snd x with
-    | None -> raise Not_found
-    | Some g -> g loc n name in
-  interp_numeral_gen loc f n (List.fold_right push_scope scopes !scope_stack)
+let interp_prim_token_cases_pattern loc p name scopes =
+  let f x = match snd x with None -> raise Not_found | Some g -> g name in
+  interp_prim_token_gen loc f p (push_scopes scopes !scope_stack)
 
-let uninterp_numeral c =
+let uninterp_prim_token c =
   try 
-    let (sc,numpr,_) = Hashtbl.find numeral_key_table (rawconstr_key c) in
+    let (sc,numpr,_) = Hashtbl.find prim_token_key_table (rawconstr_key c) in
     match numpr c with
       | None -> raise No_match
       | Some n -> (sc,n)
   with Not_found -> raise No_match
 
-let uninterp_cases_numeral c =
+let uninterp_prim_token_cases_pattern c =
   try 
-    match Hashtbl.find numeral_key_table (pattern_key c) with
+    match Hashtbl.find prim_token_key_table (pattern_key c) with
       | (_,_,None) -> raise No_match
       | (sc,_,Some numpr) ->
 	  match numpr c with
@@ -350,8 +381,8 @@ let uninterp_cases_numeral c =
 	    | Some n -> (sc,n)
   with Not_found -> raise No_match
 
-let availability_of_numeral printer_scope scopes =
-  let f scope = Hashtbl.mem numeral_interpreter_tab scope in
+let availability_of_prim_token printer_scope scopes =
+  let f scope = Hashtbl.mem prim_token_interpreter_tab scope in
   option_app snd (find_without_delimiters f (Some printer_scope,None) scopes)
 
 (* Miscellaneous *)
diff --git a/interp/notation.mli b/interp/notation.mli
index 896d427932..314efe4b6a 100644
--- a/interp/notation.mli
+++ b/interp/notation.mli
@@ -50,36 +50,45 @@ val push_scope : scope_name -> scopes -> scopes
 val declare_delimiters : scope_name -> delimiters -> unit
 val find_delimiters_scope : loc -> delimiters -> scope_name
 
-(*s Declare and uses back and forth a numeral interpretation *)
+(*s Declare and uses back and forth an interpretation of primitive token *)
 
 (* 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 num_interpreter =
-    (loc -> bigint -> rawconstr)
-    * (loc -> bigint -> name -> cases_pattern) option
+type required_module = global_reference * string list 
 
-type num_uninterpreter =
-    rawconstr list * (rawconstr -> bigint option)
-    * (cases_pattern -> bigint option) option
+type 'a prim_token_interpreter =
+    (loc -> 'a -> rawconstr) * (loc -> 'a -> name -> cases_pattern) option
+
+type 'a prim_token_uninterpreter =
+    rawconstr list * (rawconstr -> 'a option)
+    * (cases_pattern -> 'a option) option
 
-type required_module = global_reference * string list 
 val declare_numeral_interpreter : scope_name -> required_module ->
-  num_interpreter -> num_uninterpreter -> unit
+  bigint prim_token_interpreter -> bigint prim_token_uninterpreter -> unit
+
+val declare_string_interpreter : scope_name -> required_module ->
+  string prim_token_interpreter -> string prim_token_uninterpreter -> unit
+
+(* Return the [term]/[cases_pattern] bound to a primitive token in a
+   given scope context*)
+
+val interp_prim_token : loc -> prim_token -> scope_name list -> rawconstr
+val interp_prim_token_cases_pattern : loc -> prim_token -> name -> 
+  scope_name list -> cases_pattern
 
-(* Return the [term]/[cases_pattern] bound to a numeral in a given scope context*)
-val interp_numeral : loc -> bigint -> scope_name list -> rawconstr
-val interp_numeral_as_pattern : loc -> bigint -> name -> scope_name list ->
-  cases_pattern
+(* Return the primitive token associated to a [term]/[cases_pattern];
+   raise [No_match] if no such token *)
 
-(* Return the numeral bound to a [term]/[cases_pattern]; raise [No_match] if no *)
-(* such numeral *)
-val uninterp_numeral : rawconstr -> scope_name * bigint
-val uninterp_cases_numeral : cases_pattern -> scope_name * bigint
+val uninterp_prim_token : 
+  rawconstr -> scope_name * prim_token
+val uninterp_prim_token_cases_pattern : 
+  cases_pattern -> scope_name * prim_token
 
-val availability_of_numeral : scope_name -> scopes -> delimiters option option
+val availability_of_prim_token : 
+  scope_name -> scopes -> delimiters option option
 
 (*s Declare and interpret back and forth a notation *)
 
@@ -103,9 +112,8 @@ val uninterp_cases_pattern_notations : cases_pattern ->
       (interp_rule * interpretation * int option) list
 
 (* Test if a notation is available in the scopes *)
-(* context [scopes] if available, the result is not None; the first *)
-(* argument is itself not None if a delimiters is needed; the second *)
-(* argument is a numeral printer if the *)
+(* context [scopes]; if available, the result is not None; the first *)
+(* argument is itself not None if a delimiters is needed *)
 val availability_of_notation : scope_name option * notation -> scopes -> 
   (scope_name option * delimiters option) option
 
@@ -156,4 +164,4 @@ val declare_notation_printing_rule : notation -> unparsing_rule -> unit
 val find_notation_printing_rule : notation -> unparsing_rule
 
 (**********************************************************************)
-(* Rem: printing rules for numerals are trivial *)
+(* Rem: printing rules for primitive token are canonical *)
diff --git a/interp/topconstr.ml b/interp/topconstr.ml
index c75cc8575d..ad21e5b371 100644
--- a/interp/topconstr.ml
+++ b/interp/topconstr.ml
@@ -469,13 +469,15 @@ type explicitation = ExplByPos of int | ExplByName of identifier
 
 type proj_flag = int option (* [Some n] = proj of the n-th visible argument *)
 
+type prim_token = Numeral of Bigint.bigint | String of string
+
 type cases_pattern_expr =
   | CPatAlias of loc * cases_pattern_expr * identifier
   | CPatCstr of loc * reference * cases_pattern_expr list
   | CPatAtom of loc * reference option
   | CPatOr of loc * cases_pattern_expr list
   | CPatNotation of loc * notation * cases_pattern_expr list
-  | CPatNumeral of loc * Bigint.bigint
+  | CPatPrim of loc * prim_token
   | CPatDelimiters of loc * string * cases_pattern_expr
 
 type constr_expr =
@@ -502,7 +504,7 @@ type constr_expr =
   | CSort of loc * rawsort
   | CCast of loc * constr_expr * cast_kind * constr_expr
   | CNotation of loc * notation * constr_expr list
-  | CNumeral of loc * Bigint.bigint
+  | CPrim of loc * prim_token
   | CDelimiters of loc * string * constr_expr
   | CDynamic of loc * Dyn.t
 
@@ -550,7 +552,7 @@ let constr_loc = function
   | CSort (loc,_) -> loc
   | CCast (loc,_,_,_) -> loc
   | CNotation (loc,_,_) -> loc
-  | CNumeral (loc,_) -> loc
+  | CPrim (loc,_) -> loc
   | CDelimiters (loc,_,_) -> loc
   | CDynamic _ -> dummy_loc
 
@@ -560,7 +562,7 @@ let cases_pattern_loc = function
   | CPatAtom (loc,_) -> loc
   | CPatOr (loc,_) -> loc
   | CPatNotation (loc,_,_) -> loc
-  | CPatNumeral (loc,_) -> loc
+  | CPatPrim (loc,_) -> loc
   | CPatDelimiters (loc,_,_) -> loc
 
 let occur_var_constr_ref id = function
@@ -582,7 +584,7 @@ let rec occur_var_constr_expr id = function
     occur_var_constr_expr id a or occur_var_constr_expr id b
   | CNotation (_,_,l) -> List.exists (occur_var_constr_expr id) l
   | CDelimiters (loc,_,a) -> occur_var_constr_expr id a
-  | CHole _ | CEvar _ | CPatVar _ | CSort _ | CNumeral _ | CDynamic _ -> false
+  | CHole _ | CEvar _ | CPatVar _ | CSort _ | CPrim _ | CDynamic _ -> false
   | CCases (loc,_,_,_) 
   | CLetTuple (loc,_,_,_,_) 
   | CIf (loc,_,_,_,_) 
@@ -653,7 +655,7 @@ let map_constr_expr_with_binders f g e = function
   | CNotation (loc,n,l) -> CNotation (loc,n,List.map (f e) l)
   | CDelimiters (loc,s,a) -> CDelimiters (loc,s,f e a)
   | CHole _ | CEvar _ | CPatVar _ | CSort _ 
-  | CNumeral _ | CDynamic _ | CRef _ as x -> x
+  | CPrim _ | CDynamic _ | CRef _ as x -> x
   | CCases (loc,rtnpo,a,bl) ->
       (* TODO: apply g on the binding variables in pat... *)
       let bl = List.map (fun (loc,pat,rhs) -> (loc,pat,f e rhs)) bl in
diff --git a/interp/topconstr.mli b/interp/topconstr.mli
index e0f5ad5778..c7cc74b0f8 100644
--- a/interp/topconstr.mli
+++ b/interp/topconstr.mli
@@ -70,13 +70,15 @@ type explicitation = ExplByPos of int | ExplByName of identifier
 
 type proj_flag = int option (* [Some n] = proj of the n-th visible argument *)
 
+type prim_token = Numeral of Bigint.bigint | String of string
+
 type cases_pattern_expr =
   | CPatAlias of loc * cases_pattern_expr * identifier
   | CPatCstr of loc * reference * cases_pattern_expr list
   | CPatAtom of loc * reference option
   | CPatOr of loc * cases_pattern_expr list
   | CPatNotation of loc * notation * cases_pattern_expr list
-  | CPatNumeral of loc * Bigint.bigint
+  | CPatPrim of loc * prim_token
   | CPatDelimiters of loc * string * cases_pattern_expr
 
 type constr_expr =
@@ -103,7 +105,7 @@ type constr_expr =
   | CSort of loc * rawsort
   | CCast of loc * constr_expr * cast_kind * constr_expr
   | CNotation of loc * notation * constr_expr list
-  | CNumeral of loc * Bigint.bigint
+  | CPrim of loc * prim_token
   | CDelimiters of loc * string * constr_expr
   | CDynamic of loc * Dyn.t
 
diff --git a/parsing/egrammar.ml b/parsing/egrammar.ml
index 37dc007ee0..336f741aec 100644
--- a/parsing/egrammar.ml
+++ b/parsing/egrammar.ml
@@ -70,7 +70,7 @@ let make_constr_action
 	  make ((p,CRef (Ident (dummy_loc,v))) :: env) tl)
     | Some (p, ETBigint) :: tl -> (* non-terminal *)
         Gramext.action (fun (v:Bigint.bigint) ->
-	  make ((p,CNumeral (dummy_loc,v)) :: env) tl)
+	  make ((p,CPrim (dummy_loc,Numeral v)) :: env) tl)
     | Some (p, ETConstrList _) :: tl ->
         Gramext.action (fun (v:constr_expr list) ->
           let dummyid = Ident (dummy_loc,id_of_string "") in
@@ -96,7 +96,7 @@ let make_cases_pattern_action
 	  make ((p,CPatAtom (dummy_loc,Some (Ident (dummy_loc,v)))) :: env) tl)
     | Some (p, ETBigint) :: tl -> (* non-terminal *)
         Gramext.action (fun (v:Bigint.bigint) ->
-	  make ((p,CPatNumeral (dummy_loc,v)) :: env) tl)
+	  make ((p,CPatPrim (dummy_loc,Numeral v)) :: env) tl)
     | Some (p, ETConstrList _) :: tl ->
         Gramext.action (fun (v:cases_pattern_expr list) ->
           let dummyid = Ident (dummy_loc,id_of_string "") in
diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4
index 1f84221113..6208952d32 100644
--- a/parsing/g_constr.ml4
+++ b/parsing/g_constr.ml4
@@ -180,7 +180,7 @@ GEXTEND Gram
       | c=match_constr -> c
       | "("; c = operconstr LEVEL "200"; ")" ->
           (match c with
-              CNumeral(_,z) when Bigint.is_pos_or_zero z ->
+              CPrim (_,Numeral z) when Bigint.is_pos_or_zero z ->
                 CNotation(loc,"( _ )",[c])
             | _ -> c) ] ]
   ;
@@ -218,8 +218,9 @@ GEXTEND Gram
   ;
   atomic_constr:
     [ [ g=global -> CRef g
-      | s=sort -> CSort(loc,s)
-      | n=INT -> CNumeral (loc, Bigint.of_string n)
+      | s=sort -> CSort (loc,s)
+      | n=INT -> CPrim (loc, Numeral (Bigint.of_string n))
+      | s=string -> CPrim (loc, String s)
       | "_" -> CHole loc
       | "?"; id=ident -> CPatVar(loc,(false,id)) ] ]
   ;
@@ -294,10 +295,11 @@ GEXTEND Gram
       | "_" -> CPatAtom (loc,None)
       | "("; p = pattern LEVEL "200"; ")" ->
           (match p with
-              CPatNumeral(_,z) when Bigint.is_pos_or_zero z ->
+              CPatPrim (_,Numeral z) when Bigint.is_pos_or_zero z ->
                 CPatNotation(loc,"( _ )",[p])
             | _ -> p)
-      | n = INT -> CPatNumeral (loc, Bigint.of_string n) ] ]
+      | n = INT -> CPatPrim (loc, Numeral (Bigint.of_string n))
+      | s = string -> CPatPrim (loc, String s) ] ]
   ;
   binder_list:
     [ [ idl=LIST1 name; bl=LIST0 binder_let -> 
diff --git a/parsing/g_natsyntax.ml b/parsing/g_natsyntax.ml
index d80cc5ec36..073a689167 100644
--- a/parsing/g_natsyntax.ml
+++ b/parsing/g_natsyntax.ml
@@ -99,4 +99,5 @@ let _ =
   Notation.declare_numeral_interpreter "nat_scope"
     (glob_nat,["Coq";"Init";"Datatypes"])
     (nat_of_int,Some pat_nat_of_int)
-    ([RRef (dummy_loc,glob_S); RRef (dummy_loc,glob_O)], uninterp_nat, None)
+    ([RRef (dummy_loc,glob_S); RRef (dummy_loc,glob_O)], 
+     uninterp_nat, Some uninterp_nat_pattern)
diff --git a/parsing/ppconstr.ml b/parsing/ppconstr.ml
index 36470c13dc..2f2f0773b4 100644
--- a/parsing/ppconstr.ml
+++ b/parsing/ppconstr.ml
@@ -19,6 +19,7 @@ open Ppextend
 open Topconstr
 open Term
 open Pattern
+open Rawterm
 (*i*)
 
 let sep_p = fun _ -> str"."
@@ -54,6 +55,10 @@ let prec_less child (parent,assoc) =
       | Prec n -> child<=n
       | Any -> true
 
+let prec_of_prim_token = function
+  | Numeral p -> if Bigint.is_pos_or_zero p then lposint else lnegint
+  | String _ -> latom
+
 let env_assoc_value v env =
   try List.nth env (v-1)
   with Not_found -> anomaly ("Inconsistent environment for pretty-print rule")
@@ -104,8 +109,6 @@ let pr_with_comments loc pp = pr_located (fun x -> x) (loc,pp)
 
 let pr_sep_com sep f c = pr_with_comments (constr_loc c) (sep() ++ f c)
 
-open Rawterm
-
 let pr_opt pr = function
   | None -> mt ()
   | Some x -> spc() ++ pr x
@@ -157,6 +160,10 @@ let pr_or_var pr = function
   | Genarg.ArgArg x -> pr x
   | Genarg.ArgVar (loc,s) -> pr_lident (loc,s)
 
+let pr_prim_token = function
+  | Numeral n -> Bigint.pr_bigint n
+  | String s -> qs s
+
 let las = lapp
 let lpator = 100
 
@@ -174,7 +181,7 @@ let rec pr_patt sep inh p =
   | CPatNotation (_,"( _ )",[p]) ->
       pr_patt (fun()->str"(") (max_int,E) p ++ str")", latom
   | CPatNotation (_,s,env) -> pr_patnotation (pr_patt mt) s env
-  | CPatNumeral (_,i) -> Bigint.pr_bigint i, latom
+  | CPatPrim (_,p) -> pr_prim_token p, latom
   | CPatDelimiters (_,k,p) -> pr_delimiters k (pr_patt mt lsimple p), 1
   in
   let loc = cases_pattern_loc p in
@@ -566,9 +573,7 @@ let rec pr sep inherited a =
   | CNotation (_,"( _ )",[t]) ->
       pr (fun()->str"(") (max_int,L) t ++ str")", latom
   | CNotation (_,s,env) -> pr_notation (pr mt) s env
-  | CNumeral (_,p) ->
-      Bigint.pr_bigint p, 
-      (if Bigint.is_pos_or_zero p then lposint else lnegint)
+  | CPrim (_,p) -> pr_prim_token p, prec_of_prim_token p
   | CDelimiters (_,sc,a) -> pr_delimiters sc (pr mt lsimple a), 1
   | CDynamic _ -> str "<dynamic>", latom
   in
@@ -666,8 +671,6 @@ let pr_unfold_occ pr_ref = function
 
 let pr_qualid qid = str (string_of_qualid qid)
 
-open Rawterm
-
 let pr_arg pr x = spc () ++ pr x
 
 let pr_red_flag pr r =