diff options
author | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-09-12 14:51:05 +0000 |
---|---|---|
committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-09-12 14:51:05 +0000 |
commit | 296d226de9b058a69ce2f5951468c9ae11965b24 (patch) | |
tree | 539cf188e58ff65f90c7e0356cc9abd5f32c6292 | |
parent | b175b9f4714d6410b53643f7ce278a0c5770b4bf (diff) |
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
-rw-r--r-- | parsing/g_natsyntax.ml | 2 | ||||
-rw-r--r-- | parsing/g_natsyntaxnew.ml | 2 | ||||
-rw-r--r-- | parsing/g_rsyntax.ml | 2 | ||||
-rw-r--r-- | parsing/g_rsyntaxnew.ml | 2 | ||||
-rw-r--r-- | parsing/g_zsyntax.ml | 4 | ||||
-rw-r--r-- | 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 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); |