diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2006-09-23 07:39:28 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2006-09-23 07:39:28 +0000 |
| commit | 9936e2ba36e1d16dcee047d34b0c4caf8c377726 (patch) | |
| tree | 2d8e43949545cdf48e8727e4b49cf8a5c5ef7234 /.depend.camlp4 | |
| parent | 7ed3805888f7bf974b1e984c8315982442da8627 (diff) | |
- Correction filtrage des notations impliquant un "match" : la présence
des localisations empêchait toute unification des pattern de filtrage
de réussir.
- Ajout au passage d'unification des pattern modulo alpha.
- Exemples dans Notations.v
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9163 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to '.depend.camlp4')
0 files changed, 0 insertions, 0 deletions