aboutsummaryrefslogtreecommitdiff
path: root/kernel/type_errors.ml
diff options
context:
space:
mode:
authorherbelin1999-10-24 14:32:08 +0000
committerherbelin1999-10-24 14:32:08 +0000
commit349b1b788e6d77290275463f82d71a373674a98c (patch)
tree6bab83b3ca349d28decbc2867df12a47b643e6d3 /kernel/type_errors.ml
parent577e393fd4003dd406332759055ebbcfabaabd69 (diff)
Type ML des termes non prétypés
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@117 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel/type_errors.ml')
0 files changed, 0 insertions, 0 deletions