diff options
| author | herbelin | 2001-10-03 14:14:46 +0000 |
|---|---|---|
| committer | herbelin | 2001-10-03 14:14:46 +0000 |
| commit | 4c1ef79b64d4f2c7e3a730d07e103fb4e608dc68 (patch) | |
| tree | d1f817cbb66a0db69a3f395c9e3dc3f2fc58fc9e /dev | |
| parent | f7e959dda9153033683469668b0d31bd08464b5c (diff) | |
Bug de synthèse du prédicat en présence d'arguments non filtrable; correction pour prendre en compte les définitions locales dans le type des inductifs filtrés
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2101 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'dev')
0 files changed, 0 insertions, 0 deletions