aboutsummaryrefslogtreecommitdiff
path: root/parsing/g_zsyntax.ml
diff options
context:
space:
mode:
authorherbelin2005-05-20 15:54:50 +0000
committerherbelin2005-05-20 15:54:50 +0000
commitd0a324eef4d35a87e300a2b660b26fdbe2043d92 (patch)
treed223b5752d1421944fc0bcffcaf2ec49661d7114 /parsing/g_zsyntax.ml
parentf95411d169c8d636e980de3a38bb02c72c3b4965 (diff)
Adoption du nom canonique global_of_constr pour éviter confusion avec type reference
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7052 85f007b7-540e-0410-9357-904b9bb8a0f7
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 9ca72e18a7..82e651b4e0 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",