aboutsummaryrefslogtreecommitdiff
path: root/interp/dune
diff options
context:
space:
mode:
authorEmilio Jesus Gallego Arias2018-10-16 14:55:30 +0200
committerEmilio Jesus Gallego Arias2020-08-27 19:03:33 +0200
commit094e4649c29e2426daca0476c140439de901dafe (patch)
treeb6ae0cbed1ef81a84807c4d376dd610b2b2d7bbd /interp/dune
parenta87c09c13028502ea86a553724a4131c5246145a (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 'interp/dune')
-rw-r--r--interp/dune2
1 files changed, 1 insertions, 1 deletions
diff --git a/interp/dune b/interp/dune
index e9ef7ba99a..6d73d5724c 100644
--- a/interp/dune
+++ b/interp/dune
@@ -3,4 +3,4 @@
(synopsis "Coq's Syntactic Interpretation for AST [notations, implicits]")
(public_name coq.interp)
(wrapped false)
- (libraries pretyping))
+ (libraries zarith pretyping))