aboutsummaryrefslogtreecommitdiffhomepage
path: root/dev/ci
diff options
context:
space:
mode:
authorGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2017-11-08 18:00:00 +0100
committerGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2017-11-08 18:04:13 +0100
commitd7da4e1dfc58942ceb91fb24afe4751d6fb50cc9 (patch)
tree700b0b9c3dd7b29fe88a843e2f55fd9ffc296932 /dev/ci
parent0d81e80a09db7d352408be4dfc5ba263f6ed98ef (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/ci')
0 files changed, 0 insertions, 0 deletions