aboutsummaryrefslogtreecommitdiff
path: root/kernel/type_errors.ml
diff options
context:
space:
mode:
authorHugo Herbelin2016-04-13 07:56:44 +0200
committerHugo Herbelin2016-06-16 17:43:28 +0200
commit456ced60ef1fc71f8f914e07b80831fa6dd46ea5 (patch)
tree682d4dc2ef0715ce8b5232f8eb5e347b1a1d0603 /kernel/type_errors.ml
parenta43562b661115bebb9353db6ec3b2f6f8dd603ef (diff)
Fixing printing of Instance.
Diffstat (limited to 'kernel/type_errors.ml')
0 files changed, 0 insertions, 0 deletions