MAJ ZArith; contraintes plus faibles pour decider la capacite a interpreter les numeraux

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

3 files changed, 19 insertions, 13 deletions

diff --git a/parsing/g_natsyntax.ml b/parsing/g_natsyntax.ml
index dd1edf5ad..400a7f849 100644
--- a/parsing/g_natsyntax.ml
+++ b/parsing/g_natsyntax.ml
@@ -189,7 +189,7 @@ let uninterp_nat_pattern p =
 
 let _ =
   Symbols.declare_numeral_interpreter "nat_scope"
-    ["Coq";"Init";"Datatypes"]
+    (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)
 
diff --git a/parsing/g_rsyntax.ml b/parsing/g_rsyntax.ml
index 7596e1f8a..936adcc26 100644
--- a/parsing/g_rsyntax.ml
+++ b/parsing/g_rsyntax.ml
@@ -167,6 +167,7 @@ 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_R = ConstRef (make_path rdefinitions "R")
 let glob_R1 = ConstRef (make_path rdefinitions "R1")
 let glob_R0 = ConstRef (make_path rdefinitions "R0")
 let glob_Ropp = ConstRef (make_path rdefinitions "Ropp")
@@ -282,7 +283,7 @@ let uninterp_r p =
     None
 
 let _ = Symbols.declare_numeral_interpreter "R_scope"
-  ["Coq";"Reals";"Rdefinitions"]
+  (glob_R,["Coq";"Reals";"Rdefinitions"])
   ((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)],
diff --git a/parsing/g_zsyntax.ml b/parsing/g_zsyntax.ml
index b5d96a685..bfed29341 100644
--- a/parsing/g_zsyntax.ml
+++ b/parsing/g_zsyntax.ml
@@ -79,18 +79,22 @@ let _ =
 (**********************************************************************)
 (* Old v7 ast printing *)
 
+open Coqlib
+
 exception Non_closed_number
 
 let get_z_sign_ast loc =
   let ast_of_id id = 
-    Termast.ast_of_ref (Nametab.locate (Libnames.make_short_qualid id))
+    Termast.ast_of_ref
+      (reference_of_constr
+	(gen_constant_in_modules "Z-printer" zarith_base_modules id))
   in
-  ((ast_of_id (id_of_string "xI"),
-    ast_of_id (id_of_string "xO"),
-    ast_of_id (id_of_string "xH")),
-   (ast_of_id (id_of_string "ZERO"), 
-    ast_of_id (id_of_string "POS"),
-    ast_of_id (id_of_string "NEG")))
+  ((ast_of_id "xI",
+    ast_of_id "xO",
+    ast_of_id "xH"),
+   (ast_of_id "ZERO", 
+    ast_of_id "POS",
+    ast_of_id "NEG"))
 
 let _ = if !Options.v7 then
 let rec bignat_of_pos c1 c2 c3 p =
@@ -158,6 +162,7 @@ let make_path dir id = Libnames.encode_kn dir id
 
 let positive_path = 
   make_path (make_dir positive_module) (id_of_string "positive")
+let glob_positive = IndRef (positive_path,0)
 let path_of_xI = ((positive_path,0),1)
 let path_of_xO = ((positive_path,0),2)
 let path_of_xH = ((positive_path,0),3)
@@ -219,7 +224,7 @@ let uninterp_positive p =
 (***********************************************************************)
 
 let _ = Symbols.declare_numeral_interpreter "positive_scope"
-  positive_module
+  (glob_positive,positive_module)
   (interp_positive,Some pat_interp_positive)
   ([RRef (dummy_loc, glob_xI); 
     RRef (dummy_loc, glob_xO); 
@@ -283,7 +288,7 @@ let uninterp_n p =
 (* Declaring interpreters and uninterpreters for N *)
 
 let _ = Symbols.declare_numeral_interpreter "N_scope"
-  binnat_module
+  (glob_n,binnat_module)
   (n_of_int,Some pat_n_of_int)
   ([RRef (dummy_loc, glob_N0); 
     RRef (dummy_loc, glob_Npos)],
@@ -294,7 +299,7 @@ let _ = Symbols.declare_numeral_interpreter "N_scope"
 (* Parsing Z via scopes                                               *)
 (**********************************************************************)
 
-let fast_integer_module = ["Coq";"ZArith";"fast_integer"]
+let fast_integer_module = ["Coq";"ZArith";"BinInt"]
 let z_path = make_path (make_dir fast_integer_module) (id_of_string "Z")
 let glob_z = IndRef (z_path,0)
 let path_of_ZERO = ((z_path,0),1)
@@ -347,7 +352,7 @@ let uninterp_z p =
 (* Declaring interpreters and uninterpreters for Z *)
 
 let _ = Symbols.declare_numeral_interpreter "Z_scope"
-  fast_integer_module
+  (glob_z,fast_integer_module)
   (z_of_int,Some pat_z_of_int)
   ([RRef (dummy_loc, glob_ZERO); 
     RRef (dummy_loc, glob_POS);