diff --git a/tools/debug_printers b/tools/debug_printers new file mode 100644 index 00000000000..118a6b03657 --- /dev/null +++ b/tools/debug_printers @@ -0,0 +1,4 @@ +load_printer "tools/debug_printers.cmo" +install_printer Debug_printers.type_expr +install_printer Debug_printers.ident +install_printer Debug_printers.path diff --git a/tools/debug_printers.ml b/tools/debug_printers.ml new file mode 100644 index 00000000000..3b6d4603e60 --- /dev/null +++ b/tools/debug_printers.ml @@ -0,0 +1,5 @@ + +let type_expr = Printtyp.raw_type_expr +let ident = Ident.print_with_scope +let path = Path.print +