summaryrefslogtreecommitdiff
path: root/pretyping/pretype_errors.ml
diff options
context:
space:
mode:
authorGravatar Enrico Tassi <gareuselesinge@debian.org>2015-01-25 14:43:14 +0100
committerGravatar Enrico Tassi <gareuselesinge@debian.org>2015-01-25 14:43:14 +0100
commitcec4741afacd2e80894232850eaf9f9c0e45d6d7 (patch)
treee4197645da03dc3c7cc84e434cc31d0a0cca7056 /pretyping/pretype_errors.ml
parent7cfc4e5146be5666419451bdd516f1f3f264d24a (diff)
Imported Upstream version 8.5~beta1+dfsgupstream/8.5_beta1+dfsg
Diffstat (limited to 'pretyping/pretype_errors.ml')
0 files changed, 0 insertions, 0 deletions