diff options
Diffstat (limited to 'dev/top_printers.mli')
| -rw-r--r-- | dev/top_printers.mli | 1 |
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 |