1 files changed, 2 insertions, 128 deletions
diff --git a/parsing/g_natsyntax.ml b/parsing/g_natsyntax.ml
index 85b79d8bf..d80cc5ec3 100644
--- a/parsing/g_natsyntax.ml
+++ b/parsing/g_natsyntax.ml
@@ -8,105 +8,14 @@
 
 (* $Id$ *)
 
-(* This file to allow writing (3) for (S (S (S O))) 
-   and still write (S y) for (S y) *)
+(* This file defines the printer for natural numbers in [nat] *)
 
+(*i*)
 open Pcoq
 open Pp
 open Util
 open Names
-open Coqast
-open Ast
 open Coqlib
-open Termast
-open Extend
-
-let ast_O = ast_of_ref glob_O
-let ast_S = ast_of_ref glob_S
-
-(* For example, (nat_of_string "3") is <<(S (S (S O)))>> *)
-let nat_of_int n dloc =
-  let ast_O = set_loc dloc ast_O in
-  let ast_S = set_loc dloc ast_S in
-  let rec mk_nat n =
-    if n <= 0 then 
-      ast_O
-    else 
-      Node(dloc,"APPLIST", [ast_S; mk_nat (n-1)])
-  in 
-  mk_nat n
-
-let pat_nat_of_int n dloc =
-  let ast_O = set_loc dloc ast_O in
-  let ast_S = set_loc dloc ast_S in
-  let rec mk_nat n =
-    if n <= 0 then 
-      ast_O
-    else 
-      Node(dloc,"PATTCONSTRUCT", [ast_S; mk_nat (n-1)])
-  in 
-  mk_nat n
-
-let nat_of_string s dloc = 
-  nat_of_int (int_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) ->
-	(int_of_nat_rec astS astO a)+1
-    | a when alpha_eq(a,astO) -> 1  
-          (***** YES, 1, non 0 ... to print the successor of p *)
-    | _ -> raise Non_closed_number
-	  
-let int_of_nat p =
-  try 
-    Some (int_of_nat_rec ast_S ast_O p)
-  with
-    Non_closed_number -> None
-
-let pr_S a = hov 0 (str "S" ++ brk (1,1) ++ a)
-
-let rec pr_external_S std_pr = function
-  | Node (l,"APPLIST", [b; a]) when alpha_eq (b,ast_S) ->
-      str"(" ++ pr_S (pr_external_S std_pr a) ++ str")"
-  | p -> std_pr p
-
-(* Declare the primitive printer *)
-
-(* Prints not p, but the SUCCESSOR of p !!!!! *)
-let nat_printer std_pr p =
-  match (int_of_nat p) with
-    | Some i -> str "(" ++ str (string_of_int i) ++ str ")"
-    | None -> str "(" ++ pr_S (pr_external_S std_pr p) ++ str ")"
-
-let _ = Esyntax.Ppprim.add ("nat_printer", nat_printer)
-(*
-(* Declare the primitive parser *)
-
-let unat = create_univ_if_new "nat"
-
-let number = create_constr_entry unat "number" 
-let pat_number = create_constr_entry unat "pat_number"
- 
-let _ = 
-  Gram.extend number None
-    [None, None,
-     [[Gramext.Stoken ("INT", "")],
-      Gramext.action nat_of_string]]
-
-let _ = 
-  Gram.extend pat_number None
-    [None, None,
-     [[Gramext.Stoken ("INT", "")],
-      Gramext.action pat_nat_of_string]]
-*)
-
-(*i*)
 open Rawterm
 open Libnames
 open Bigint
@@ -191,38 +100,3 @@ let _ =
     (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)
-
-(************************************************************************)
-(* Old ast printing *)
-
-open Coqast
-open Ast
-open Termast
-
-let _ = if !Options.v7 then
-let ast_O = ast_of_ref glob_O in
-let ast_S = ast_of_ref glob_S in
-
-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
-in
-(* 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
-in
-let nat_printer_O _ =
-  Some (int 0)
-in
-(* Declare the primitive printers *)
-let _ =
-  Esyntax.declare_primitive_printer "nat_printer_S" "nat_scope" nat_printer_S
-in
-let _ = 
-  Esyntax.declare_primitive_printer "nat_printer_O" "nat_scope" nat_printer_O
-in
-()