diff options
Diffstat (limited to 'dev')
| -rw-r--r-- | dev/set_raw_db | 1 | ||||
| -rw-r--r-- | dev/top_printers.ml | 3 |
2 files changed, 3 insertions, 1 deletions
diff --git a/dev/set_raw_db b/dev/set_raw_db new file mode 100644 index 0000000000..5caff7e5d4 --- /dev/null +++ b/dev/set_raw_db @@ -0,0 +1 @@ +install_printer Top_printers.ppconstrdb diff --git a/dev/top_printers.ml b/dev/top_printers.ml index df089f0b1b..df3835d2fe 100644 --- a/dev/top_printers.ml +++ b/dev/top_printers.ml @@ -46,7 +46,8 @@ let ppsp sp = pp(pr_sp sp) let ppqualid qid = pp(pr_qualid qid) (* term printers *) -let ppconstr x = pp(Termops.print_constr x) +let ppconstr x = pp (Termops.print_constr x) +let ppconstrdb x = pp(Options.with_option Constrextern.rawdebug Termops.print_constr x) let ppterm = ppconstr let ppsconstr x = ppconstr (Declarations.force x) let ppconstr_univ x = Constrextern.with_universes ppconstr x |