diff options
| author | courtieu | 2003-03-31 12:52:38 +0000 |
|---|---|---|
| committer | courtieu | 2003-03-31 12:52:38 +0000 |
| commit | 8a8b61d623dd1a37cf5a7edb4d77ba8cae893085 (patch) | |
| tree | 7cce7e4d048ea48bc2ba408a14c3e25ddbdf6cab /dev | |
| parent | f5bdbc026f6aa9456aa3850451942f72f9c9190e (diff) | |
Correcting a bug occuring when the mimicked function had a
lambda-abstraction inside a Cases. I had to make the term of the
induction principle a bit less clean (more eta expansions).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3817 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'dev')
0 files changed, 0 insertions, 0 deletions