aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/nativenorm.ml
diff options
context:
space:
mode:
authorGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2014-11-22 15:20:04 +0100
committerGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2014-11-22 19:23:33 +0100
commitc3bb115fa765278bc3bcb3beb8c74b0fb8b35d98 (patch)
treed4c6a1f78ec210d8b0100144251ca236ff1902cd /pretyping/nativenorm.ml
parentb3320b0f942a9f86d5bd1c00876f8816e5c94446 (diff)
Specific printer of Evar.Set.t for ocamldebug + more information in
a UserError to ease debugging.
Diffstat (limited to 'pretyping/nativenorm.ml')
0 files changed, 0 insertions, 0 deletions