aboutsummaryrefslogtreecommitdiff
path: root/kernel/type_errors.ml
diff options
context:
space:
mode:
authorherbelin2006-06-23 10:52:28 +0000
committerherbelin2006-06-23 10:52:28 +0000
commit81200e25dec5cb3ee37f3ec6b153d130900258a8 (patch)
treecb70197e7bac3bde4d01dc71cd4a4edc7e166688 /kernel/type_errors.ml
parenteacab552644acdaf9922d831a09e8318f9c96980 (diff)
Nouveau paragraphe sur le polymorphisme de sorte des inductifs
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8980 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel/type_errors.ml')
0 files changed, 0 insertions, 0 deletions