aboutsummaryrefslogtreecommitdiffhomepage
path: root/contrib/correctness
diff options
context:
space:
mode:
Diffstat (limited to 'contrib/correctness')
-rw-r--r--contrib/correctness/psyntax.ml45
1 files changed, 3 insertions, 2 deletions
diff --git a/contrib/correctness/psyntax.ml4 b/contrib/correctness/psyntax.ml4
index 8e4c9b2bd..9e3e8a1bb 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)