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 /toplevel | |
| 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 'toplevel')
| -rw-r--r-- | toplevel/dune | 4 |
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)) |