aboutsummaryrefslogtreecommitdiffhomepage
path: root/dev/top_printers.ml
diff options
context:
space:
mode:
Diffstat (limited to 'dev/top_printers.ml')
-rw-r--r--dev/top_printers.ml3
1 files changed, 2 insertions, 1 deletions
diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index 3116cbf22..c765f3848 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -9,6 +9,7 @@
(* Printers for the ocaml toplevel. *)
open System
+open Errors
open Util
open Pp
open Names
@@ -131,7 +132,7 @@ let pppftreestate p = pp(print_pftreestate p)
(* let pr_glls glls = *)
(* hov 0 (pr_evar_defs (sig_sig glls) ++ fnl () ++ *)
-(* prlist_with_sep pr_fnl db_pr_goal (sig_it glls)) *)
+(* prlist_with_sep fnl db_pr_goal (sig_it glls)) *)
(* let ppsigmagoal g = pp(pr_goal (sig_it g)) *)
(* let prgls gls = pp(pr_gls gls) *)