diff options
| author | Emilio Jesus Gallego Arias | 2018-10-16 14:55:30 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2020-08-27 19:03:33 +0200 |
| commit | 094e4649c29e2426daca0476c140439de901dafe (patch) | |
| tree | b6ae0cbed1ef81a84807c4d376dd610b2b2d7bbd /toplevel | |
| parent | a87c09c13028502ea86a553724a4131c5246145a (diff) | |
[numeral] [plugins] Switch from `Big_int` to ZArith.
We replace Coq's use of `Big_int` and `num` by the ZArith OCaml
library which is a more modern version.
We switch the core files and easy plugins only for now, more complex
numerical plugins will be done in their own commit.
We thus keep the num library linked for now until all plugins are
ported.
Co-authored-by: Vincent Laporte <Vincent.Laporte@fondation-inria.fr>
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/dune | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/toplevel/dune b/toplevel/dune index 2d64ae303c..5f10346ac4 100644 --- a/toplevel/dune +++ b/toplevel/dune @@ -3,8 +3,9 @@ (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)) -; Coqlevel provides the `Num` library to plugins, we could also use +; Interp provides the `zarith` library to plugins, we could also use ; -linkall in the plugins file, to be discussed. (coq.pp (modules g_toplevel)) |