suppression doublon

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

2 files changed, 0 insertions, 228 deletions

diff --git a/theories/Arith/g_natsyntax.ml b/theories/Arith/g_natsyntax.ml
deleted file mode 100644
index ff5c5b948..000000000
--- a/theories/Arith/g_natsyntax.ml
+++ /dev/null
@@ -1,78 +0,0 @@
-
-(* $Id;$ *)
-
-(* This file to allow writing (3) for (S (S (S O))) 
-   and still write (S y) for (S y) *)
-
-open Util
-open Pcoq
-open Pp
-open Names
-open Coqast
-open Ast
-
-exception Non_closed_number
-
-let get_nat_sign loc =
-  let ast_of_id id = Astterm.globalize_command (Nvar(loc,id)) in
-  (ast_of_id "O", ast_of_id "S", ast_of_id "My_special_variable")
-
-(* For example, (nat_of_string "3") is <<(S (S (S O)))>> *)
-let nat_of_int n dloc =
-  let (astO,astS,_) = get_nat_sign dloc in
-  let rec mk_nat n =
-    if n <= 0 then 
-      astO
-    else 
-      Node(dloc,"APPLIST", [astS; mk_nat (n-1)])
-  in 
-  mk_nat n
-
-let nat_of_string s dloc = nat_of_int (int_of_string s) dloc
-
-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 =
-  let (astO,astS,_) = get_nat_sign dummy_loc in
-  try 
-    Some (int_of_nat_rec astS astO p)
-  with
-    Non_closed_number -> None
-
-let replace_S p = 
-  let (_,astS,astmyvar) = get_nat_sign dummy_loc in
-  let rec aux p =
-    match p with
-      | Node (l,"APPLIST", [b; a]) when b = astS ->
-          Node (l, "APPLIST", [astmyvar; (aux a)])
-      | _ -> p
-  in 
-  ope("APPLIST", [astmyvar; (aux 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 (string_of_int i) >]
-    | None -> std_pr (replace_S p)
-
-let _ = Esyntax.Ppprim.add ("nat_printer", nat_printer)
-
-(* Declare the primitive parser *)
-open Pcoq
-
-let number = 
-  match create_entry (get_univ "nat") "number" ETast with
-    | Ast n -> n
-    | _ -> anomaly "G_natsyntax : create_entry number failed"
-
-let _ = 
-  Gram.extend number None
-    [None, None, [[Gramext.Stoken ("INT", "")], Gramext.action nat_of_string]]
diff --git a/theories/Zarith/g_zsyntax.ml b/theories/Zarith/g_zsyntax.ml
deleted file mode 100644
index 85ebb140a..000000000
--- a/theories/Zarith/g_zsyntax.ml
+++ /dev/null
@@ -1,150 +0,0 @@
-
-(* $Id$ *)
-
-open Coqast
-open Pcoq
-open Util
-open Pp
-open Names
-open Ast
-
-let get_z_sign loc =
-  let ast_of_id id = Astterm.globalize_command (Nvar(loc,id)) in
-  ((ast_of_id "xI", ast_of_id "xO", ast_of_id "xH"),
-   (ast_of_id "ZERO", ast_of_id "POS", ast_of_id "NEG"),
-   (ast_of_id "My_special_variable0", ast_of_id "My_special_variable1"))
-
-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 =
-  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 ?"
-  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
-  if is_nonzero v then
-    if pos_or_neg then
-      ope("APPLIST",[astPOS; pos_of_int_array astxI astxO astxH v])
-    else 
-      ope("APPLIST",[astNEG; pos_of_int_array astxI astxO astxH v])
-  else 
-    astZERO
-
-exception Non_closed_number
-
-let rec int_array_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)
-    | 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 |]
-    | _ -> raise Non_closed_number
-
-let int_array_option_of_pos astxI astxO astxH p =
-  try Some (int_array_of_pos astxO astxI astxH p)
-  with Non_closed_number -> None
-
-let inside_printer posneg std_pr p = 
-  let ((astxI,astxO,astxH),_,(myvar0,myvar1)) = get_z_sign dummy_loc in
-  match (int_array_option_of_pos astxI astxO astxH p) with
-    | Some n -> 
-	if posneg 
-	then [< 'sTR (string_of_int_array n) >]
-	else [< 'sTR "(-"; 'sTR (string_of_int_array n); 'sTR ")" >]
-    | None -> 
-	let c = if posneg then myvar0 else myvar1 in
-	std_pr (ope("ZEXPR",[ope("APPLIST",[c; p])]))
-
-let outside_printer posneg std_pr p = 
-  let ((astxI,astxO,astxH),_,(myvar0,myvar1)) = get_z_sign dummy_loc in
-  match (int_array_option_of_pos astxI astxO astxH p) with
-    | Some n -> 
-	if posneg 
-	then [< 'sTR "`"; 'sTR (string_of_int_array n); 'sTR "`">]
-        else [< 'sTR "`-"; 'sTR (string_of_int_array n); 'sTR "`" >]
-    | None -> 
-	let c = if posneg then myvar0 else myvar1 in
-	[< 'sTR "("; std_pr (ope("APPLIST",[c; p])); 'sTR ")" >] 
-
-(* Declare pretty-printers for integers *)
-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 *)
-open Pcoq
-
-let number = 
-  match create_entry (get_univ "znatural") "number" ETast with
-    | Ast n -> n 
-    | _ -> anomaly "G_zsyntax.number"
-	  
-let negnumber = 
-  match create_entry (get_univ "znatural") "negnumber" ETast with
-    | Ast n -> n 
-    | _ -> anomaly "G_zsyntax.negnumber"
-
-let _ = 
-  Gram.extend number None
-    [None, None,
-     [[Gramext.Stoken ("INT", "")],
-      Gramext.action (z_of_string true)]]
-
-let _ = 
-  Gram.extend negnumber None
-    [None, None,
-     [[Gramext.Stoken ("INT", "")],
-      Gramext.action (z_of_string false)]]