diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2006-01-30 23:10:11 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2006-01-30 23:10:11 +0000 |
| commit | 5545e216c21c13ed1cd5560af0b373796f40d0c4 (patch) | |
| tree | 1b8e52e18f641e68724823ea79c5c009d8c7bd2e /pretyping/cases.mli | |
| parent | f4161c9cc9b19f1061e1d3d6f3caf75317b18bde (diff) | |
- Prise en compte de la clause 'in I' pour coercer le type du terme à filtrer
- Prise en compte coercions autour des sous-termes filtrés (si non dépendants)
- Test du bon nombre d'argument des constructeurs (et de l'inductif si
clause "in I ...") maintenant fait aussi dans constrintern, pour
assurer notamment que les constructeurs et inductifs dans pattern
(obtenu de rawconstr) ont les bonnes arités
- Renommage v7 -> v8 dans commentaires
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7959 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'pretyping/cases.mli')
0 files changed, 0 insertions, 0 deletions