diff options
Diffstat (limited to 'parsing')
-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); |