MAJ module requis pour le parsing des numéraux

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

6 files changed, 8 insertions, 8 deletions

diff --git a/parsing/g_natsyntax.ml b/parsing/g_natsyntax.ml
index 1d91a949f..f206a74b6 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";"Peano"]
+    ["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_natsyntaxnew.ml b/parsing/g_natsyntaxnew.ml
index b124c4ec0..912a0594c 100644
--- a/parsing/g_natsyntaxnew.ml
+++ b/parsing/g_natsyntaxnew.ml
@@ -190,6 +190,6 @@ let uninterp_nat_pattern p =
 
 let _ =
   Symbols.declare_numeral_interpreter "nat_scope"
-    ["Coq";"Init";"Peano"]
+    ["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 13eb76334..2c0e9da77 100644
--- a/parsing/g_rsyntax.ml
+++ b/parsing/g_rsyntax.ml
@@ -219,7 +219,7 @@ let uninterp_r p =
     None
 
 let _ = Symbols.declare_numeral_interpreter "R_scope"
-  ["Coq";"Reals";"Rsyntax"]
+  ["Coq";"Reals";"Rdefinitions"]
   (r_of_int2,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_rsyntaxnew.ml b/parsing/g_rsyntaxnew.ml
index 081762ae3..408fbb9f3 100644
--- a/parsing/g_rsyntaxnew.ml
+++ b/parsing/g_rsyntaxnew.ml
@@ -105,7 +105,7 @@ let uninterp_r p =
     None
 
 let _ = Symbols.declare_numeral_interpreter "R_scope"
-  ["Coq";"Reals";"Rsyntax"]
+  ["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)],
diff --git a/parsing/g_zsyntax.ml b/parsing/g_zsyntax.ml
index 11c88d113..7f286bcae 100644
--- a/parsing/g_zsyntax.ml
+++ b/parsing/g_zsyntax.ml
@@ -216,7 +216,7 @@ let uninterp_positive p =
 (***********************************************************************)
 
 let _ = Symbols.declare_numeral_interpreter "positive_scope"
-  ["Coq";"ZArith";"Zsyntax"]
+  ["Coq";"ZArith";"fast_integer_module"]
   (interp_positive,Some pat_interp_positive)
   ([RRef (dummy_loc, glob_xI); 
     RRef (dummy_loc, glob_xO); 
@@ -280,7 +280,7 @@ let uninterp_z p =
 (* Declaring interpreters and uninterpreters for Z *)
 
 let _ = Symbols.declare_numeral_interpreter "Z_scope"
-  ["Coq";"ZArith";"Zsyntax"]
+  ["Coq";"ZArith";"fast_integer"]
   (z_of_int,Some pat_z_of_int)
   ([RRef (dummy_loc, glob_ZERO); 
     RRef (dummy_loc, glob_POS); 
diff --git a/parsing/g_zsyntaxnew.ml b/parsing/g_zsyntaxnew.ml
index 24b6d4137..668d0e587 100644
--- a/parsing/g_zsyntaxnew.ml
+++ b/parsing/g_zsyntaxnew.ml
@@ -95,7 +95,7 @@ let uninterp_positive p =
 (***********************************************************************)
 
 let _ = Symbols.declare_numeral_interpreter "positive_scope"
-  ["Coq";"ZArith";"Zsyntax"]
+  ["Coq";"ZArith";"fast_integer"]
   (interp_positive,Some pat_interp_positive)
   ([RRef (dummy_loc, glob_xI); 
     RRef (dummy_loc, glob_xO); 
@@ -159,7 +159,7 @@ let uninterp_z p =
 (* Declaring interpreters and uninterpreters for Z *)
 
 let _ = Symbols.declare_numeral_interpreter "Z_scope"
-  ["Coq";"ZArith";"Zsyntax"]
+  ["Coq";"ZArith";"fast_integer"]
   (z_of_int,Some pat_z_of_int)
   ([RRef (dummy_loc, glob_ZERO); 
     RRef (dummy_loc, glob_POS);