aboutsummaryrefslogtreecommitdiffhomepage
path: root/parsing/g_zsyntax.ml
diff options
context:
space:
mode:
Diffstat (limited to 'parsing/g_zsyntax.ml')
-rw-r--r--parsing/g_zsyntax.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/parsing/g_zsyntax.ml b/parsing/g_zsyntax.ml
index 9ca72e18a..82e651b4e 100644
--- a/parsing/g_zsyntax.ml
+++ b/parsing/g_zsyntax.ml
@@ -86,7 +86,7 @@ exception Non_closed_number
let get_z_sign_ast loc =
let ast_of_id id =
Termast.ast_of_ref
- (reference_of_constr
+ (global_of_constr
(gen_constant_in_modules "Z-printer" zarith_base_modules id))
in
((ast_of_id "xI",