Partly realize some missing theories of ieee_float.

Makefile.in

@@ -955,7 +955,7 @@ COQLIBS_FP_FILES = Rounding SingleFormat Single DoubleFormat Double
 COQLIBS_FP_ALL_FILES = GenFloat $(COQLIBS_FP_FILES)
 COQLIBS_FP = $(addprefix lib/coq/floating_point/, $(COQLIBS_FP_ALL_FILES))
 
-COQLIBS_IEEEFLOAT_FILES = GenericFloat
+COQLIBS_IEEEFLOAT_FILES = RoundingMode GenericFloat Float32 Float64
 COQLIBS_IEEEFLOAT = $(addprefix lib/coq/ieee_float/, $(COQLIBS_IEEEFLOAT_FILES))
 endif
 

lib/coq/ieee_float/RoundingMode.v

+(********************************************************************)
+(*                                                                  *)
+(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
+(*  Copyright 2010-2017   --   INRIA - CNRS - Paris-Sud University  *)
+(*                                                                  *)
+(*  This software is distributed under the terms of the GNU Lesser  *)
+(*  General Public License version 2.1, with the special exception  *)
+(*  on linking described in file LICENSE.                           *)
+(*                                                                  *)
+(********************************************************************)
+
+(* This file is generated by Why3's Coq-realize driver *)
+(* Beware! Only edit allowed sections below    *)
+Require Import BuiltIn.
+Require BuiltIn.
+
+(* Why3 assumption *)
+Inductive mode :=
+  | RNE : mode
+  | RNA : mode
+  | RTP : mode
+  | RTN : mode
+  | RTZ : mode.
+Axiom mode_WhyType : WhyType mode.
+Existing Instance mode_WhyType.
+
+(* Why3 assumption *)
+Definition to_nearest (m:mode): Prop := (m = RNE) \/ (m = RNA).
+