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

1 files changed, 9 insertions, 8 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
+()