aboutsummaryrefslogtreecommitdiff
path: root/kernel/type_errors.ml
diff options
context:
space:
mode:
authorHugo Herbelin2014-07-14 12:36:30 +0200
committerHugo Herbelin2014-07-15 18:15:52 +0200
commit6afdf9bd419e0353924789c6c0d5d92ecdae2f46 (patch)
treead8a5efbcadd128382c83a999faa88d5f8308a57 /kernel/type_errors.ml
parentec94edf830ff9676c43c86f0eb9038c4bd205f62 (diff)
Some basics facts about eq_dep.
Diffstat (limited to 'kernel/type_errors.ml')
0 files changed, 0 insertions, 0 deletions