diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2004-08-24 14:30:15 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2004-08-24 14:30:15 +0000 |
| commit | d63e8fab799f643c6fbb7c4f586ba52c9799e56d (patch) | |
| tree | f50f8c67228281d149450c26b0d68d933a7c81c9 /kernel/doc.tex | |
| parent | 49b72354838e1381cf2cea8cc84e452e93480426 (diff) | |
Expansion du prédicat du 'match' vis à vis de la dépendance en le terme filtré (utilisation de Anonymous pour signaler une dépendance formelle, en relation avec le nommage dans Inductiveops.type_case_branches); uniformisation/nettoyage
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6032 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel/doc.tex')
0 files changed, 0 insertions, 0 deletions