From d39fab9a7c39d8da868c4481b96cf1086c21b1a4 Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Thu, 10 Oct 2019 20:11:02 +0200 Subject: Fix ldshiftexp * Fix the implementations and add tests * Change shift from int63 to Z (was always used as a Z) * Update FloatLemmas.v accordingly Co-authored-by: Erik Martin-Dorel --- kernel/uint63.mli | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) (limited to 'kernel/uint63.mli') diff --git a/kernel/uint63.mli b/kernel/uint63.mli index 7ed3d415e4..e0bf44da35 100644 --- a/kernel/uint63.mli +++ b/kernel/uint63.mli @@ -19,8 +19,10 @@ val to_int2 : t -> int * int (* msb, lsb *) val of_int64 : Int64.t -> t (* val of_uint : int -> t -*) -val to_int_saturate : t -> int (* maxuint31 in case of overflow *) + *) +(** [int_min n m] returns the minimum of [n] and [m], + [m] must be in [0, 2^30-1]. *) +val to_int_min : t -> int -> int (* conversion to float *) val of_float : float -> t -- cgit v1.2.3