diff options
| author | Emilio Jesus Gallego Arias | 2020-09-16 22:00:38 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2020-09-17 15:28:03 +0200 |
| commit | 29b8aae282f03fcd7d753d19129e5f74feacc820 (patch) | |
| tree | 583b907530ea9c77bdec3d1bf11488f7ef5d00c1 /INSTALL.md | |
| parent | 2eb778033fe37fa26adaf41d48fc630ef66c9d1d (diff) | |
[install] Rewording of primitive floats.
As suggested in the PR review.
Co-authored-by: Jim Fehrle <jim.fehrle@gmail.com>
Diffstat (limited to 'INSTALL.md')
| -rw-r--r-- | INSTALL.md | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/INSTALL.md b/INSTALL.md index c0ae5e5677..51d59e1638 100644 --- a/INSTALL.md +++ b/INSTALL.md @@ -32,11 +32,11 @@ To compile Coq yourself, you need: (version >= 3.0.beta8), and the corresponding GTK 3.x libraries, as of today (gtk+3 >= 3.18 and gtksourceview3 >= 3.18) -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. +Primitive floating-point numbers require IEEE-754 compliance +(`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 proving `False` on this architecture. Note that OCaml dependencies (`zarith` and `lablgtk3-sourceview3` at this moment) must be properly registered with `findlib/ocamlfind` |