From 296d226de9b058a69ce2f5951468c9ae11965b24 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Fri, 12 Sep 2003 14:51:05 +0000
Subject: 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
---
 parsing/g_natsyntax.ml    | 2 +-
 parsing/g_natsyntaxnew.ml | 2 +-
 parsing/g_rsyntax.ml      | 2 +-
 parsing/g_rsyntaxnew.ml   | 2 +-
 parsing/g_zsyntax.ml      | 4 ++--
 parsing/g_zsyntaxnew.ml   | 4 ++--
 6 files changed, 8 insertions(+), 8 deletions(-)

diff --git a/parsing/g_natsyntax.ml b/parsing/g_natsyntax.ml
index 1d91a949f9..f206a74b64 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 b124c4ec08..912a0594c5 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 13eb763347..2c0e9da774 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 081762ae37..408fbb9f3c 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 11c88d113e..7f286bcae8 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 24b6d4137d..668d0e587f 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); 
-- 
cgit v1.2.3