diff options
| author | Hugo Herbelin | 2017-11-08 18:00:00 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2017-11-08 18:04:13 +0100 |
| commit | d7da4e1dfc58942ceb91fb24afe4751d6fb50cc9 (patch) | |
| tree | 700b0b9c3dd7b29fe88a843e2f55fd9ffc296932 /dev/db | |
| parent | 0d81e80a09db7d352408be4dfc5ba263f6ed98ef (diff) | |
Adding a debugging printer for ident maps whose codomain type is unknown.
Actually, ocaml is apparently doing well. If there is a printer for 'a
Id.Map.t and another for say Id.t Id.Map.id, it uses the most defined
existing ones, so, it is apparently not a problem to have overlapping
printer.
Diffstat (limited to 'dev/db')
| -rw-r--r-- | dev/db | 1 |
1 files changed, 1 insertions, 0 deletions
@@ -68,5 +68,6 @@ install_printer Top_printers.ppist install_printer Top_printers.ppconstrunderbindersidmap install_printer Top_printers.ppunbound_ltac_var_map install_printer Top_printers.ppididmap +install_printer Top_printers.ppidmapgen install_printer Top_printers.ppclosure install_printer Top_printers.ppclosedglobconstr |