aboutsummaryrefslogtreecommitdiff
path: root/kernel/type_errors.ml
diff options
context:
space:
mode:
authorfilliatr1999-11-19 17:01:43 +0000
committerfilliatr1999-11-19 17:01:43 +0000
commit9bdaa212057cdd41ba416cc9f05167e91eeed4b3 (patch)
tree328de03d16931d5abfd9ac4c0254b93cb0e5dcf9 /kernel/type_errors.ml
parentb0382a9829f08282351244839526bd2ffbe6283f (diff)
module Pattern, Wcclausenv (interface) et Tacticals
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@126 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel/type_errors.ml')
0 files changed, 0 insertions, 0 deletions