diff options
| author | Emilio Jesus Gallego Arias | 2020-09-10 21:58:31 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2020-09-17 15:27:48 +0200 |
| commit | 2eb778033fe37fa26adaf41d48fc630ef66c9d1d (patch) | |
| tree | e28252dc8d989e9e5c43b87e2e37044372a35661 /toplevel/dune | |
| parent | 14f0e5059e7f49cabbcd1571d7f053db7d7d3f35 (diff) | |
[build] Don't link `num` anymore in Coq
After #8743 we don't depend on `num` anymore in the codebase; thus we
drop the dependency.
This could create problems for plugins relying on this implicit
linking.
Diffstat (limited to 'toplevel/dune')
| -rw-r--r-- | toplevel/dune | 7 |
1 files changed, 3 insertions, 4 deletions
diff --git a/toplevel/dune b/toplevel/dune index 5f10346ac4..0256d1ec96 100644 --- a/toplevel/dune +++ b/toplevel/dune @@ -3,9 +3,8 @@ (public_name coq.toplevel) (synopsis "Coq's Interactive Shell [terminal-based]") (wrapped false) - ; num still here due to some plugins using it - (libraries num coq.stm)) -; Interp provides the `zarith` library to plugins, we could also use -; -linkall in the plugins file, to be discussed. + (libraries coq.stm)) +; Interp does provides the `zarith` library to plugins, we could also +; use -linkall in the plugins file, to be discussed. (coq.pp (modules g_toplevel)) |