aboutsummaryrefslogtreecommitdiffhomepage
path: root/dev/top_printers.ml
diff options
context:
space:
mode:
authorGravatar Amin Timany <amintimany@gmail.com>2017-06-15 16:50:05 +0200
committerGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2017-06-16 04:52:11 +0200
commit15b1856edd593b39d63d23584a4f5acec0eeb592 (patch)
tree4233f58e213573b48bfd2692af758b30f385db7c /dev/top_printers.ml
parenta4969591f391d857a9efd038338e1a80fc68950b (diff)
Fix a bug in cumulativity
Diffstat (limited to 'dev/top_printers.ml')
-rw-r--r--dev/top_printers.ml1
1 files changed, 0 insertions, 1 deletions
diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index abf6db1b7..ff575e432 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -8,7 +8,6 @@
(* Printers for the ocaml toplevel. *)
-open API
open Util
open Pp
open Names