From e641aeeef1cde745561593b7ef9edb0112712cbf Mon Sep 17 00:00:00 2001
From: herbelin
Date: Thu, 28 Nov 2002 23:02:54 +0000
Subject: Court-circuit de g_zsyntax

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3329 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 contrib/correctness/psyntax.ml4 | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

diff --git a/contrib/correctness/psyntax.ml4 b/contrib/correctness/psyntax.ml4
index 8e4c9b2bd3..9e3e8a1bbb 100644
--- a/contrib/correctness/psyntax.ml4
+++ b/contrib/correctness/psyntax.ml4
@@ -94,8 +94,9 @@ module Programs =
 
 open Programs
 
-let ast_of_int n =
-  G_zsyntax.z_of_string true n dummy_loc
+let ast_of_int n = 
+  CDelimiters
+    (dummy_loc, "Z", CNumeral (dummy_loc, Bignat.POS (Bignat.of_string n)))
 
 let constr_of_int n =
   Constrintern.interp_constr Evd.empty (Global.env ()) (ast_of_int n)
-- 
cgit v1.2.3