diff options
| author | herbelin | 2011-11-16 08:46:46 +0000 |
|---|---|---|
| committer | herbelin | 2011-11-16 08:46:46 +0000 |
| commit | 93b759f35a9f6544c5da9643330beb54ce255619 (patch) | |
| tree | 6990924e40d883eff674d60a0270bcd3e74a39a9 /kernel/type_errors.ml | |
| parent | 73e164c4bbb495703222a026e0b405c5b0bbb547 (diff) | |
Old typing bug in pattern-matching compilation (apparently w/o
consequences up to now, but maybe because this type is often later on
thrown away).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14663 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel/type_errors.ml')
0 files changed, 0 insertions, 0 deletions