diff options
Diffstat (limited to 'dev')
| -rw-r--r-- | dev/db | 2 | ||||
| -rw-r--r-- | dev/top_printers.ml | 4 |
2 files changed, 6 insertions, 0 deletions
@@ -2,6 +2,8 @@ load_printer "gramlib.cma" load_printer "str.cma" load_printer "printers.cma" +install_printer Top_printers.ppfuture + install_printer Top_printers.ppid install_printer Top_printers.ppidset install_printer Top_printers.ppevar diff --git a/dev/top_printers.ml b/dev/top_printers.ml index 6f2c241767..7d6370b9d5 100644 --- a/dev/top_printers.ml +++ b/dev/top_printers.ml @@ -31,6 +31,10 @@ let _ = Detyping.set_detype_anonymous (fun _ _ -> raise Not_found) (* std_ppcmds *) let pppp x = pp x +(** Future printer *) + +let ppfuture kx = pp (Future.print (fun _ -> str "_") kx) + (* name printers *) let ppid id = pp (pr_id id) let pplab l = pp (pr_lab l) |