Unused constant in stdlib/floating_point
floating_point.SingleFull module, constant
min_single is defined but it's unused
(The same is true of
DoubleFull module) .
I think that it should be the following:
module SingleFull use export SingleFormat constant min_single : real = 0x1p-149 clone export GenFloatSpecFull with type t = single, constant max = max_single, constant max_representable_integer = max_int, constant min = min_single, (* Added by me *) lemma Bounded_real_no_overflow end