From 29b8aae282f03fcd7d753d19129e5f74feacc820 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Wed, 16 Sep 2020 22:00:38 +0200 Subject: [install] Rewording of primitive floats. As suggested in the PR review. Co-authored-by: Jim Fehrle --- INSTALL.md | 10 +++++----- toplevel/dune | 4 ++-- 2 files changed, 7 insertions(+), 7 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` diff --git a/toplevel/dune b/toplevel/dune index 0256d1ec96..98f4ba2edf 100644 --- a/toplevel/dune +++ b/toplevel/dune @@ -4,7 +4,7 @@ (synopsis "Coq's Interactive Shell [terminal-based]") (wrapped false) (libraries coq.stm)) -; Interp does provides the `zarith` library to plugins, we could also -; use -linkall in the plugins file, to be discussed. +; Interp provides the `zarith` library to plugins, we could also use +; -linkall in the plugins file, to be discussed. (coq.pp (modules g_toplevel)) -- cgit v1.2.3