Merge PR #9867: Add primitive floats (binary64 floating-point numbers)

Ack-by: SkySkimmer
Reviewed-by: Zimmi48
Ack-by: ejgallego
Reviewed-by: maximedenes
Ack-by: proux01
Ack-by: silene
Ack-by: vbgl

1 files changed, 10 insertions, 0 deletions

diff --git a/INSTALL b/INSTALL
index e30706e005..d9efd55b95 100644
--- a/INSTALL
+++ b/INSTALL
@@ -21,9 +21,19 @@ WHAT DO YOU NEED ?
 
    - a C compiler
 
+   - an IEEE-754 compliant architecture with rounding to nearest
+     ties to even as default rounding mode (most architectures
+     should work nowadays)
+
    - for CoqIDE, the lablgtk development files (version >= 3.0.0),
      and the GTK 3.x libraries including gtksourceview3.
 
+   The IEEE-754 compliance is required by primitive floating-point
+   numbers (Require Import Floats). Common sources of incompatibility
+   are checked at configure time, preventing compilation. In the,
+   unlikely, event an incompatibility remains undetected, using Floats
+   would enable to prove False on this architecture.
+
    Note that num and lablgtk should be properly registered with
    findlib/ocamlfind as Coq's makefile will use it to locate the
    libraries during the build.