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 --- toplevel/dune | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'toplevel') 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