aboutsummaryrefslogtreecommitdiff
path: root/kernel/type_errors.mli
diff options
context:
space:
mode:
authorGuillaume Melquiond2014-04-28 13:56:51 +0200
committerGuillaume Melquiond2014-04-28 13:58:37 +0200
commit49162693b37a3bebc47cd6f667b2e7ebea209fc6 (patch)
treeeb3a22097961339805c4166a84e3bffc4b99a66f /kernel/type_errors.mli
parent2bcb2cb8ddadbaf2e5b6d4abbfdbdf3bc88cc4c6 (diff)
Fix broken commit 2bcb2cb.
Diffstat (limited to 'kernel/type_errors.mli')
0 files changed, 0 insertions, 0 deletions