Fusion des g_*syntaxnew.ml avec les g_*syntax.ml avec sélection dynamique selon

l'option v7


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

6 files changed, 122 insertions, 531 deletions

diff --git a/parsing/g_natsyntax.ml b/parsing/g_natsyntax.ml
index f206a74b6..502123833 100644
--- a/parsing/g_natsyntax.ml
+++ b/parsing/g_natsyntax.ml
@@ -200,29 +200,30 @@ open Coqast
 open Ast
 open Termast
 
-let ast_O = ast_of_ref glob_O
-let ast_S = ast_of_ref glob_S
-
-exception Non_closed_number
+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
+()
diff --git a/parsing/g_natsyntaxnew.ml b/parsing/g_natsyntaxnew.ml
deleted file mode 100644
index 912a0594c..000000000
--- a/parsing/g_natsyntaxnew.ml
+++ /dev/null
@@ -1,195 +0,0 @@
-(***********************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
-(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
-(*   \VV/  *************************************************************)
-(*    //   *      This file is distributed under the terms of the      *)
-(*         *       GNU Lesser General Public License Version 2.1       *)
-(***********************************************************************)
-
-(* $Id$ *)
-
-(* This file to allow writing (3) for (S (S (S O))) 
-   and still write (S y) for (S y) *)
-
-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 Bignat
-open Coqlib
-open Symbols
-open Pp
-open Util
-open Names
-(*i*)
-
-(**********************************************************************)
-(* Parsing via scopes *)
-(* For example, (nat_of_string "3") is <<(S (S (S O)))>> *)
-
-let nat_of_int dloc n =
-  match n with
-  | 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 acc n =
-	if is_nonzero n then 
-	  mk_nat (RApp (dloc,ref_S, [acc])) (sub_1 n)
-	else 
-	  acc
-      in 
-      mk_nat ref_O 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")
-
-(***********************************************************************)
-(* Printing via scopes *)
-
-exception Non_closed_number
-
-let rec int_of_nat = function
-  | RApp (_,RRef (_,s),[a]) when s = glob_S -> add_1 (int_of_nat a)
-  | RRef (_,z) when z = glob_O -> zero
-  | _ -> raise Non_closed_number
-	  
-let uninterp_nat p =
-  try 
-    Some (POS (int_of_nat p))
-  with
-    Non_closed_number -> None
-
-let rec int_of_nat_pattern = function
-  | PatCstr (_,s,[a],_) when ConstructRef s = glob_S ->
-      add_1 (int_of_nat_pattern a)
-  | PatCstr (_,z,[],_) when ConstructRef z = glob_O -> zero
-  | _ -> raise Non_closed_number
-	  
-let uninterp_nat_pattern p =
-  try 
-    Some (POS (int_of_nat_pattern p))
-  with
-    Non_closed_number -> None
-
-(***********************************************************************)
-(* Declare the primitive parsers and printers *)
-
-let _ =
-  Symbols.declare_numeral_interpreter "nat_scope"
-    ["Coq";"Init";"Datatypes"]
-    (nat_of_int,Some pat_nat_of_int)
-    ([RRef (dummy_loc,glob_S); RRef (dummy_loc,glob_O)], uninterp_nat, None)
diff --git a/parsing/g_rsyntax.ml b/parsing/g_rsyntax.ml
index 2c0e9da77..7596e1f8a 100644
--- a/parsing/g_rsyntax.ml
+++ b/parsing/g_rsyntax.ml
@@ -51,6 +51,7 @@ if m< 2 then [m]
 else let (x1,x2) = div2 m in x1::(list_ch x2)
 in list_ch n
 
+let _ = if !Options.v7 then
 let r_of_int n dloc =
   let (a0,a1,plus,mult,_,_) = get_r_sign dloc in
   let list_ch = int_decomp n in
@@ -62,23 +63,24 @@ let r_of_int n dloc =
     | a::[b] -> if a==1 then mkAppC (plus, [a1; a2]) else a2
     | a::l' -> if a=1 then mkAppC (plus, [a1; mkAppC (mult, [a2; mk_r l'])]) else mkAppC (mult, [a2; mk_r l'])
   in mk_r list_ch
-
+in
 let r_of_string s dloc = 
   r_of_int (int_of_string s) dloc
-
+in
 let rsyntax_create name =
   let e =
     Pcoq.create_constr_entry (Pcoq.get_univ "rnatural") name in
   Pcoq.Gram.Unsafe.clear_entry e;
   e
-
+in
 let rnumber = rsyntax_create "rnumber"
-
+in
 let _ = 
   Gram.extend rnumber None
     [None, None,
      [[Gramext.Stoken ("INT", "")],
       Gramext.action r_of_string]]
+in ()
 
 (**********************************************************************)
 (* Old ast printing                                                   *)
@@ -86,6 +88,7 @@ let _ =
 
 exception Non_closed_number
 
+let _ = if !Options.v7 then
 let int_of_r p =
   let (a0,a1,plus,mult,_,_) = get_r_sign_ast dummy_loc in
   let rec int_of_r_rec p = 
@@ -111,46 +114,47 @@ let int_of_r p =
     Some (int_of_r_rec p)
   with
     Non_closed_number -> None
-
+in
 let replace_plus p = 
   let (_,_,_,_,astnrplus,_) = get_r_sign_ast dummy_loc in
   ope ("REXPR",[ope("APPLIST",[astnrplus;p])])
-
+in
 let replace_mult p = 
   let (_,_,_,_,_,astnrmult) = get_r_sign_ast dummy_loc in
   ope ("REXPR",[ope("APPLIST",[astnrmult;p])])
-
+in
 let rec r_printer_odd std_pr p =
   let (_,a1,plus,_,_,_) = get_r_sign_ast dummy_loc in
   match (int_of_r (ope("APPLIST",[plus;a1;p]))) with
     | Some i -> str (string_of_int i)
     | None -> std_pr (replace_plus p)
-
+in
 let rec r_printer_odd_outside std_pr p =
   let (_,a1,plus,_,_,_) = get_r_sign_ast dummy_loc in
   match (int_of_r (ope("APPLIST",[plus;a1;p]))) with
     | Some i -> str"``" ++ str (string_of_int i) ++ str"``"
     | None -> std_pr (replace_plus p)
-
+in
 let rec r_printer_even std_pr p =
   let (_,a1,plus,mult,_,_) = get_r_sign_ast dummy_loc in
   match (int_of_r (ope("APPLIST",[mult;(ope("APPLIST",[plus;a1;a1]));p]))) with
     | Some i -> str (string_of_int i)
     | None -> std_pr (replace_mult p)
-
+in
 let rec r_printer_even_outside std_pr p =
   let (_,a1,plus,mult,_,_) = get_r_sign_ast dummy_loc in
   match (int_of_r (ope("APPLIST",[mult;(ope("APPLIST",[plus;a1;a1]));p]))) with
     | Some i -> str"``" ++ str (string_of_int i) ++ str"``"
     | None -> std_pr (replace_mult p)
-
-let _ = Esyntax.Ppprim.add ("r_printer_odd", r_printer_odd)
-let _ = Esyntax.Ppprim.add ("r_printer_odd_outside", r_printer_odd_outside)
-let _ = Esyntax.Ppprim.add ("r_printer_even", r_printer_even)
+in
+let _ = Esyntax.Ppprim.add ("r_printer_odd", r_printer_odd) in
+let _ = Esyntax.Ppprim.add ("r_printer_odd_outside", r_printer_odd_outside) in
+let _ = Esyntax.Ppprim.add ("r_printer_even", r_printer_even) in
 let _ = Esyntax.Ppprim.add ("r_printer_even_outside", r_printer_even_outside)
+in ()
 
 (**********************************************************************)
-(* Parsing Z via scopes                                               *)
+(* Parsing R via scopes                                               *)
 (**********************************************************************)
 
 open Libnames
@@ -169,6 +173,7 @@ let glob_Ropp = ConstRef (make_path rdefinitions "Ropp")
 let glob_Rplus = ConstRef (make_path rdefinitions "Rplus")
 let glob_Rmult = ConstRef (make_path rdefinitions "Rmult")
 
+(* V7 *)
 let r_of_posint dloc n =
   let ref_R0 = RRef (dloc, glob_R0) in
   let ref_R1 = RRef (dloc, glob_R1) in
@@ -191,10 +196,39 @@ let r_of_int2 dloc z =
   | NEG n -> RApp (dloc, RRef(dloc,glob_Ropp), [r_of_posint dloc (int_of_string (bigint_to_string (POS n)))]) 
   | POS n -> r_of_posint dloc (int_of_string (bigint_to_string z))
 
+(* V8 *)
+let two = mult_2 one
+let three = add_1 two
+let four = mult_2 two
+
+(* Unary representation of strictly positive numbers *)
+let rec small_r dloc n =
+  if is_one n then RRef (dloc, glob_R1)
+  else RApp(dloc,RRef (dloc,glob_Rplus),
+            [RRef (dloc, glob_R1);small_r dloc (sub_1 n)])
+
+let r_of_posint dloc n =
+  let r1 = RRef (dloc, glob_R1) in
+  let r2 = small_r dloc two in
+  let rec r_of_pos n =
+    if less_than n four then small_r dloc n
+    else
+      let (q,r) = div2_with_rest n in
+      let b = RApp(dloc,RRef(dloc,glob_Rmult),[r2;r_of_pos q]) in
+      if r then RApp(dloc,RRef(dloc,glob_Rplus),[r1;b]) else b in
+  if is_nonzero n then r_of_pos n else RRef(dloc,glob_R0)
+
+let r_of_int dloc z =
+  match z with
+  | NEG n -> RApp (dloc, RRef(dloc,glob_Ropp), [r_of_posint dloc n]) 
+  | POS n -> r_of_posint dloc n
+
 (**********************************************************************)
 (* Printing R via scopes                                              *)
 (**********************************************************************)
 
+let bignat_of_r =
+if !Options.v7 then
 let rec bignat_of_r = function
   | RApp (_,RRef (_,p), [RRef (_,o1); RRef (_,o2)]) when p = glob_Rplus & o1 = glob_R1 & o2 = glob_R1 -> add_1 one
   | RApp (_,RRef (_,p), [RRef (_,o); RApp (_,RRef (_,p2),_) as a]) when p = glob_Rplus & o = glob_R1 -> 
@@ -207,6 +241,35 @@ let rec bignat_of_r = function
   | RRef (_,a) when a = glob_R1 -> one
   | RRef (_,a) when a = glob_R0 -> zero
   | _ -> raise Non_closed_number
+in bignat_of_r
+else
+(* for numbers > 1 *)
+let rec bignat_of_pos = function
+  (* 1+1 *)
+  | RApp (_,RRef (_,p), [RRef (_,o1); RRef (_,o2)])
+      when p = glob_Rplus & o1 = glob_R1 & o2 = glob_R1 -> two
+  (* 1+1+1 *)
+  | RApp (_,RRef (_,p1), [RRef (_,o1);
+      RApp(_,RRef (_,p2),[RRef(_,o2);RRef(_,o3)])])
+      when p1 = glob_Rplus & p2 = glob_Rplus &
+           o1 = glob_R1 & o2 = glob_R1 & o3 = glob_R1 -> three
+  (* (1+1)*b *)
+  | RApp (_,RRef (_,p), [a; b]) when p = glob_Rmult ->
+      if bignat_of_pos a <> two then raise Non_closed_number;
+      mult_2 (bignat_of_pos b)
+  (* 1+(1+1)*b *)
+  | RApp (_,RRef (_,p1), [RRef (_,o); RApp (_,RRef (_,p2),[a;b])])
+      when p1 = glob_Rplus & p2 = glob_Rmult & o = glob_R1  -> 
+      if bignat_of_pos a <> two then raise Non_closed_number;
+        add_1 (mult_2 (bignat_of_pos b))
+  | _ -> raise Non_closed_number
+in
+let bignat_of_r = function
+  | RRef (_,a) when a = glob_R0 -> zero
+  | RRef (_,a) when a = glob_R1 -> one
+  | r -> bignat_of_pos r
+in
+bignat_of_r
 
 let bigint_of_r = function
   | RApp (_,RRef (_,o), [a]) when o = glob_Ropp -> NEG (bignat_of_r a)
@@ -220,7 +283,7 @@ let uninterp_r p =
 
 let _ = Symbols.declare_numeral_interpreter "R_scope"
   ["Coq";"Reals";"Rdefinitions"]
-  (r_of_int2,None)
+  ((if !Options.v7 then r_of_int2 else r_of_int),None)
   ([RRef(dummy_loc,glob_Ropp);RRef(dummy_loc,glob_R0);
     RRef(dummy_loc,glob_Rplus);RRef(dummy_loc,glob_Rmult);RRef(dummy_loc,glob_R1)],
     uninterp_r,
@@ -229,8 +292,7 @@ let _ = Symbols.declare_numeral_interpreter "R_scope"
 (***********************************************************************)
 (* Old ast printers via scope *)
 
-exception Non_closed_number
-
+let _ = if !Options.v7 then
 let bignat_of_pos p =
   let (_,one,plus,_,_,_) = get_r_sign_ast dummy_loc in
   let rec transl = function
@@ -239,35 +301,36 @@ let bignat_of_pos p =
     | a when alpha_eq(a,one) -> Bignat.one
     | _ -> raise Non_closed_number
   in transl p
-	  
+in
 let bignat_option_of_pos p =
   try 
     Some (bignat_of_pos p)
   with Non_closed_number -> 
     None
-
+in
 let r_printer_Rplus1 p =
   match bignat_option_of_pos p with
     | Some n -> Some (str (Bignat.to_string (add_1 n)))
     | None -> None
-
+in
 let r_printer_Ropp p =
   match bignat_option_of_pos p with
     | Some n -> Some (str "-" ++ str (Bignat.to_string n))
     | None -> None
-
+in
 let r_printer_R1 _ =
   Some (int 1)
-
+in
 let r_printer_R0 _ =
   Some (int 0)
-
+in
 (* Declare pretty-printers for integers *)
 let _ =
   Esyntax.declare_primitive_printer "r_printer_Ropp" "R_scope" (r_printer_Ropp)
-let _ =
+in let _ =
   Esyntax.declare_primitive_printer "r_printer_Rplus1" "R_scope" (r_printer_Rplus1)
-let _ =
+in let _ =
   Esyntax.declare_primitive_printer "r_printer_R1" "R_scope" (r_printer_R1)
-let _ =
+in let _ =
   Esyntax.declare_primitive_printer "r_printer_R0" "R_scope" r_printer_R0
+in ()
diff --git a/parsing/g_rsyntaxnew.ml b/parsing/g_rsyntaxnew.ml
deleted file mode 100644
index 408fbb9f3..000000000
--- a/parsing/g_rsyntaxnew.ml
+++ /dev/null
@@ -1,113 +0,0 @@
-(***********************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
-(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
-(*   \VV/  *************************************************************)
-(*    //   *      This file is distributed under the terms of the      *)
-(*         *       GNU Lesser General Public License Version 2.1       *)
-(***********************************************************************)
-
-open Coqast
-open Ast
-open Pp
-open Util
-open Names
-open Pcoq
-open Extend
-open Topconstr
-open Libnames
-
-(**********************************************************************)
-(* Parsing R 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 glob_Rmult = ConstRef (make_path rdefinitions "Rmult")
-
-let two = mult_2 one
-let three = add_1 two
-let four = mult_2 two
-
-(* Unary representation of strictly positive numbers *)
-let rec small_r dloc n =
-  if is_one n then RRef (dloc, glob_R1)
-  else RApp(dloc,RRef (dloc,glob_Rplus),
-            [RRef (dloc, glob_R1);small_r dloc (sub_1 n)])
-
-let r_of_posint dloc n =
-  let r1 = RRef (dloc, glob_R1) in
-  let r2 = small_r dloc two in
-  let rec r_of_pos n =
-    if less_than n four then small_r dloc n
-    else
-      let (q,r) = div2_with_rest n in
-      let b = RApp(dloc,RRef(dloc,glob_Rmult),[r2;r_of_pos q]) in
-      if r then RApp(dloc,RRef(dloc,glob_Rplus),[r1;b]) else b in
-  if is_nonzero n then r_of_pos n else RRef(dloc,glob_R0)
-
-let r_of_int dloc z =
-  match z with
-  | NEG n -> RApp (dloc, RRef(dloc,glob_Ropp), [r_of_posint dloc n]) 
-  | POS n -> r_of_posint dloc n
-
-(**********************************************************************)
-(* Printing R via scopes                                              *)
-(**********************************************************************)
-
-exception Non_closed_number
-
-(* for numbers > 1 *)
-let rec bignat_of_pos = function
-  (* 1+1 *)
-  | RApp (_,RRef (_,p), [RRef (_,o1); RRef (_,o2)])
-      when p = glob_Rplus & o1 = glob_R1 & o2 = glob_R1 -> two
-  (* 1+1+1 *)
-  | RApp (_,RRef (_,p1), [RRef (_,o1);
-      RApp(_,RRef (_,p2),[RRef(_,o2);RRef(_,o3)])])
-      when p1 = glob_Rplus & p2 = glob_Rplus &
-           o1 = glob_R1 & o2 = glob_R1 & o3 = glob_R1 -> three
-  (* (1+1)*b *)
-  | RApp (_,RRef (_,p), [a; b]) when p = glob_Rmult ->
-      if bignat_of_pos a <> two then raise Non_closed_number;
-      mult_2 (bignat_of_pos b)
-  (* 1+(1+1)*b *)
-  | RApp (_,RRef (_,p1), [RRef (_,o); RApp (_,RRef (_,p2),[a;b])])
-      when p1 = glob_Rplus & p2 = glob_Rmult & o = glob_R1  -> 
-      if bignat_of_pos a <> two then raise Non_closed_number;
-        add_1 (mult_2 (bignat_of_pos b))
-  | _ -> raise Non_closed_number
-
-let bignat_of_r = function
-  | RRef (_,a) when a = glob_R0 -> zero
-  | RRef (_,a) when a = glob_R1 -> one
-  | r -> bignat_of_pos r
-
-let bigint_of_r = function
-  | RApp (_,RRef (_,o), [a]) when o = glob_Ropp -> NEG (bignat_of_r a)
-  | a -> POS (bignat_of_r a)
-
-let uninterp_r p =
-  try
-    Some (bigint_of_r p)
-  with Non_closed_number ->
-    None
-
-let _ = Symbols.declare_numeral_interpreter "R_scope"
-  ["Coq";"Reals";"Rdefinitions"]
-  (r_of_int,None)
-  ([RRef(dummy_loc,glob_Ropp);RRef(dummy_loc,glob_R0);
-    RRef(dummy_loc,glob_Rplus);RRef(dummy_loc,glob_Rmult);RRef(dummy_loc,glob_R1)],
-    uninterp_r,
-    None)
diff --git a/parsing/g_zsyntax.ml b/parsing/g_zsyntax.ml
index 7f286bcae..0a872d7aa 100644
--- a/parsing/g_zsyntax.ml
+++ b/parsing/g_zsyntax.ml
@@ -92,6 +92,7 @@ let get_z_sign_ast loc =
     ast_of_id (id_of_string "POS"),
     ast_of_id (id_of_string "NEG")))
 
+let _ = if !Options.v7 then
 let rec bignat_of_pos c1 c2 c3 p =
   match p with
     | Node (_,"APPLIST", [b; a]) when alpha_eq(b,c1) ->
@@ -100,15 +101,15 @@ let rec bignat_of_pos c1 c2 c3 p =
         add_1 (mult_2 (bignat_of_pos c1 c2 c3 a))
     | a when alpha_eq(a,c3) -> Bignat.one
     | _ -> raise Non_closed_number
-	  
+in
 let bignat_option_of_pos xI xO xH p =
   try 
     Some (bignat_of_pos xO xI xH p)
   with Non_closed_number -> 
     None
-
-let pr_pos a = hov 0 (str "POS" ++ brk (1,1) ++ a)
-let pr_neg a = hov 0 (str "NEG" ++ brk (1,1) ++ a)
+in
+let pr_pos a = hov 0 (str "POS" ++ brk (1,1) ++ a) in
+let pr_neg a = hov 0 (str "NEG" ++ brk (1,1) ++ a) in
 
 let inside_printer posneg std_pr p =
   let ((xI,xO,xH),_) = get_z_sign_ast dummy_loc in
@@ -121,9 +122,9 @@ let inside_printer posneg std_pr p =
     | None -> 
 	let pr = if posneg then pr_pos else pr_neg in
 	str "(" ++ pr (std_pr (ope("ZEXPR",[p]))) ++ str ")"
-
+in
 let outside_zero_printer std_pr p = str "`0`"
-
+in
 let outside_printer posneg std_pr p =
   let ((xI,xO,xH),_) = get_z_sign_ast dummy_loc in
   match (bignat_option_of_pos xI xO xH p) with
@@ -135,12 +136,13 @@ let outside_printer posneg std_pr p =
       | None -> 
 	  let pr = if posneg then pr_pos else pr_neg in
 	  str "(" ++ pr (std_pr p) ++ str ")"
-
+in
 (* 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 ("positive_printer", (outside_printer true)) in
+let _ = Esyntax.Ppprim.add ("negative_printer", (outside_printer false)) in
+let _ = Esyntax.Ppprim.add ("positive_printer_inside", (inside_printer true))in
 let _ = Esyntax.Ppprim.add ("negative_printer_inside", (inside_printer false))
+in ()
 
 (**********************************************************************)
 (* Parsing positive via scopes                                        *)
@@ -216,7 +218,7 @@ let uninterp_positive p =
 (***********************************************************************)
 
 let _ = Symbols.declare_numeral_interpreter "positive_scope"
-  ["Coq";"ZArith";"fast_integer_module"]
+  ["Coq";"ZArith";"fast_integer"]
   (interp_positive,Some pat_interp_positive)
   ([RRef (dummy_loc, glob_xI); 
     RRef (dummy_loc, glob_xO); 
@@ -291,8 +293,9 @@ let _ = Symbols.declare_numeral_interpreter "Z_scope"
 (***********************************************************************)
 (* Old ast Printers *)
 
-exception Non_closed_number
+open Esyntax
 
+let _ = if !Options.v7 then
 let bignat_of_pos p =
   let ((xI,xO,xH),_) = get_z_sign_ast dummy_loc in
   let c1 = xO in
@@ -304,13 +307,13 @@ let bignat_of_pos p =
     | a when alpha_eq(a,c3) -> Bignat.one
     | _ -> raise Non_closed_number
   in transl p
-	  
+in
 let bignat_option_of_pos p =
   try 
     Some (bignat_of_pos p)
   with Non_closed_number -> 
     None
-
+in
 let z_printer posneg p =
   match bignat_option_of_pos p with
     | Some n -> 
@@ -319,15 +322,15 @@ let z_printer posneg p =
 	else 
 	  Some (str "-" ++ str (Bignat.to_string n))
     | None -> None
-
+in
 let z_printer_ZERO _ =
   Some (int 0)
-
+in
 (* Declare pretty-printers for integers *)
-open Esyntax
 let _ =
-  declare_primitive_printer "z_printer_POS" "Z_scope" (z_printer true)
+  declare_primitive_printer "z_printer_POS" "Z_scope" (z_printer true) in
 let _ =
-  declare_primitive_printer "z_printer_NEG" "Z_scope" (z_printer false)
+  declare_primitive_printer "z_printer_NEG" "Z_scope" (z_printer false) in
 let _ =
-  declare_primitive_printer "z_printer_ZERO" "Z_scope" z_printer_ZERO
+  declare_primitive_printer "z_printer_ZERO" "Z_scope" z_printer_ZERO in
+()
diff --git a/parsing/g_zsyntaxnew.ml b/parsing/g_zsyntaxnew.ml
deleted file mode 100644
index 668d0e587..000000000
--- a/parsing/g_zsyntaxnew.ml
+++ /dev/null
@@ -1,168 +0,0 @@
-(***********************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
-(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
-(*   \VV/  *************************************************************)
-(*    //   *      This file is distributed under the terms of the      *)
-(*         *       GNU Lesser General Public License Version 2.1       *)
-(***********************************************************************)
-
-(* $Id$ *)
-
-open Coqast
-open Pcoq
-open Pp
-open Util
-open Names
-open Ast
-open Extend
-open Topconstr
-open Libnames
-open Bignat
-
-(**********************************************************************)
-(* Parsing positive 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 positive_path = make_path fast_integer_module (id_of_string "positive")
-let path_of_xI = ((positive_path,0),1)
-let path_of_xO = ((positive_path,0),2)
-let path_of_xH = ((positive_path,0),3)
-let glob_xI = ConstructRef path_of_xI
-let glob_xO = ConstructRef path_of_xO
-let glob_xH = ConstructRef path_of_xH
-
-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 interp_positive dloc = function
-  | POS n when is_nonzero n -> pos_of_bignat dloc n
-  | _ ->
-      user_err_loc (dloc, "interp_positive",
-        str "Only strictly positive numbers in type \"positive\"!")
-
-let rec pat_pos_of_bignat dloc x name =
-  match div2_with_rest x with
-    | (q,false) -> 
-        PatCstr (dloc,path_of_xO,[pat_pos_of_bignat dloc q Anonymous],name)
-    | (q,true) when is_nonzero q -> 
-        PatCstr (dloc,path_of_xI,[pat_pos_of_bignat dloc q Anonymous],name)
-    | (q,true) ->
-        PatCstr (dloc,path_of_xH,[],name)
-
-let pat_interp_positive dloc = function
-  | POS n -> pat_pos_of_bignat dloc n
-  | NEG n ->
-      user_err_loc (dloc, "interp_positive",
-        str "No negative number in type \"positive\"!")
-
-(**********************************************************************)
-(* Printing positive via scopes                                       *)
-(**********************************************************************)
-
-exception Non_closed_number
-
-let rec bignat_of_pos = function
-  | RApp (_, RRef (_,b),[a]) when b = glob_xO -> mult_2(bignat_of_pos a)
-  | RApp (_, RRef (_,b),[a]) when b = glob_xI -> add_1(mult_2(bignat_of_pos a))
-  | RRef (_, a) when a = glob_xH -> Bignat.one
-  | _ -> raise Non_closed_number
-
-let uninterp_positive p =
-  try 
-    Some (POS (bignat_of_pos p))
-  with Non_closed_number -> 
-    None
-
-(***********************************************************************)
-(* Declaring interpreters and uninterpreters for positive *)
-(***********************************************************************)
-
-let _ = Symbols.declare_numeral_interpreter "positive_scope"
-  ["Coq";"ZArith";"fast_integer"]
-  (interp_positive,Some pat_interp_positive)
-  ([RRef (dummy_loc, glob_xI); 
-    RRef (dummy_loc, glob_xO); 
-    RRef (dummy_loc, glob_xH)],
-   uninterp_positive,
-   None)
-
-(**********************************************************************)
-(* Parsing Z via scopes                                               *)
-(**********************************************************************)
-
-let z_path = make_path fast_integer_module (id_of_string "Z")
-let glob_z = IndRef (z_path,0)
-let path_of_ZERO = ((z_path,0),1)
-let path_of_POS = ((z_path,0),2)
-let path_of_NEG = ((z_path,0),3)
-let glob_ZERO = ConstructRef path_of_ZERO
-let glob_POS = ConstructRef path_of_POS
-let glob_NEG = ConstructRef path_of_NEG
-
-let z_of_posint 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 z_of_int dloc z =
-  match z with
-  | POS n -> z_of_posint dloc true n 
-  | NEG n -> z_of_posint dloc false n 
-
-let pat_z_of_posint dloc pos_or_neg n name = 
-  if is_nonzero n then
-    let sgn = if pos_or_neg then path_of_POS else path_of_NEG in
-    PatCstr (dloc, sgn, [pat_pos_of_bignat dloc n Anonymous], name)
-  else 
-    PatCstr (dloc, path_of_ZERO, [], name)
-
-let pat_z_of_int dloc n name =
-  match n with
-  | POS n -> pat_z_of_posint dloc true n name
-  | NEG n -> pat_z_of_posint dloc false n name
-
-(**********************************************************************)
-(* Printing Z via scopes                                              *)
-(**********************************************************************)
-
-let bigint_of_z = function
-  | RApp (_, RRef (_,b),[a]) when b = glob_POS -> POS (bignat_of_pos a)
-  | RApp (_, RRef (_,b),[a]) when b = glob_NEG -> NEG (bignat_of_pos a)
-  | RRef (_, a) when a = glob_ZERO -> POS (Bignat.zero)
-  | _ -> raise Non_closed_number
-
-let uninterp_z p =
-  try
-    Some (bigint_of_z p)
-  with Non_closed_number -> None
-
-(***********************************************************************)
-(* Declaring interpreters and uninterpreters for Z *)
-
-let _ = Symbols.declare_numeral_interpreter "Z_scope"
-  ["Coq";"ZArith";"fast_integer"]
-  (z_of_int,Some pat_z_of_int)
-  ([RRef (dummy_loc, glob_ZERO); 
-    RRef (dummy_loc, glob_POS); 
-    RRef (dummy_loc, glob_NEG)],
-  uninterp_z,
-  None)