diff options
| author | bertot | 2001-04-10 13:50:34 +0000 |
|---|---|---|
| committer | bertot | 2001-04-10 13:50:34 +0000 |
| commit | 45d82e91c30f912740211060b4cdb7cb83226157 (patch) | |
| tree | 69aeeff425a9edaefb7139497d33720b91f13cc4 /kernel | |
| parent | 2bb2d480b547e58deb2ec62791c8990ecac777b0 (diff) | |
Modified searchPattern. Before this correction, constructors were overlooked,
because the observation was done on the internal data-structure provided in
the inductive definition. But this internal data-structure is not well-suited
pattern-matching, since it contains debruijn indices where the inductive type
should occur.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1572 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel')
0 files changed, 0 insertions, 0 deletions