aboutsummaryrefslogtreecommitdiffstats
path: root/caml/Camlcoq.ml
diff options
context:
space:
mode:
Diffstat (limited to 'caml/Camlcoq.ml')
-rw-r--r--caml/Camlcoq.ml4
1 files changed, 3 insertions, 1 deletions
diff --git a/caml/Camlcoq.ml b/caml/Camlcoq.ml
index d60e0222..e9089cf3 100644
--- a/caml/Camlcoq.ml
+++ b/caml/Camlcoq.ml
@@ -51,7 +51,9 @@ let z_of_camlint n =
if n > 0l then Zpos (positive_of_camlint n)
else Zneg (positive_of_camlint (Int32.neg n))
-let coqint_of_camlint : int32 -> Integers.int = z_of_camlint
+let coqint_of_camlint (n: int32) : Integers.int =
+ (* Interpret n as unsigned so that resulting Z is in range *)
+ if n = 0l then Z0 else Zpos (positive_of_camlint n)
(* Atoms (positive integers representing strings) *)