aboutsummaryrefslogtreecommitdiff
path: root/dev/top_printers.mli
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 /dev/top_printers.mli
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 'dev/top_printers.mli')
-rw-r--r--dev/top_printers.mli1
1 files changed, 0 insertions, 1 deletions
diff --git a/dev/top_printers.mli b/dev/top_printers.mli
index 65eab8daa3..b1bb5e4702 100644
--- a/dev/top_printers.mli
+++ b/dev/top_printers.mli
@@ -53,7 +53,6 @@ val ppglob_constr : 'a Glob_term.glob_constr_g -> unit
val pppattern : Pattern.constr_pattern -> unit
val ppfconstr : CClosure.fconstr -> unit
-val ppbigint : Bigint.bigint -> unit
val ppnumtokunsigned : NumTok.Unsigned.t -> unit
val ppnumtokunsignednat : NumTok.UnsignedNat.t -> unit