aboutsummaryrefslogtreecommitdiffhomepage
path: root/parsing/g_zsyntaxnew.ml
diff options
context:
space:
mode:
Diffstat (limited to 'parsing/g_zsyntaxnew.ml')
-rw-r--r--parsing/g_zsyntaxnew.ml4
1 files changed, 2 insertions, 2 deletions
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);