aboutsummaryrefslogtreecommitdiff
path: root/toplevel/dune
diff options
context:
space:
mode:
authorEmilio Jesus Gallego Arias2020-09-16 22:00:38 +0200
committerEmilio Jesus Gallego Arias2020-09-17 15:28:03 +0200
commit29b8aae282f03fcd7d753d19129e5f74feacc820 (patch)
tree583b907530ea9c77bdec3d1bf11488f7ef5d00c1 /toplevel/dune
parent2eb778033fe37fa26adaf41d48fc630ef66c9d1d (diff)
[install] Rewording of primitive floats.
As suggested in the PR review. Co-authored-by: Jim Fehrle <jim.fehrle@gmail.com>
Diffstat (limited to 'toplevel/dune')
-rw-r--r--toplevel/dune4
1 files changed, 2 insertions, 2 deletions
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))