From f4dcd1d9f696972e7cbdaa8d70e5abb1a18820ef Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond
Date: Wed, 2 Dec 2020 06:44:10 +0100
Subject: Make sure the msb is clear.

This is presumably not usable from the surface language. But an ML module
could easily create a proof of false by passing a negative number to
Const.mkInt.
---
 kernel/uint63_31.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/kernel/uint63_31.ml b/kernel/uint63_31.ml
index 3517f51bfc..988611df3e 100644
--- a/kernel/uint63_31.ml
+++ b/kernel/uint63_31.ml
@@ -23,9 +23,9 @@ let one = Int64.one
 
     (* conversion from an int *)
 let mask63 i = Int64.logand i maxuint63
-let of_int i = Int64.of_int i
+let of_int i = mask63 (Int64.of_int i)
 let to_int2 i = (Int64.to_int (Int64.shift_right_logical i 31), Int64.to_int i)
-let of_int64 i = i
+let of_int64 = mask63
 let to_int64 i = i
 
 let to_int_min n m =
-- 
cgit v1.2.3