diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2006-04-24 10:23:30 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2006-04-24 10:23:30 +0000 |
| commit | 36b78e4e0fccc476015d9c34c23f47df4ae5c6e0 (patch) | |
| tree | 3e7eb1f0d3f0451305b79e9874b4544aa0d7b5eb /test-suite/output/Tactics.out | |
| parent | 44038db7f052e45bb864a9878016e67120107570 (diff) | |
Timide tentative de clarification du statut de l'opérateur de filtrage
PCase dans le type pattern: le type pattern est utilisé
essentiellement dans ltac, il est normalement obtenu sans typage, et
ce via rawconstr (sauf cas de filtrage ltac non linéaire où il est
obtenu de constr). Le cas d'un filtrage sur un "if" doit être traité à
part car sans le type, il est impossible de savoir le nombre
d'arguments du constructeur puisque par définition du "if", ceux-ci ne
sont pas liants et ne laissent pas dans la syntaxe concrète
(résolution au passage du bug #1070, dû à un filtrage incomplet dans
le passage de pattern à rawconstr permettant l'affichage des pattern).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8728 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'test-suite/output/Tactics.out')
| -rw-r--r-- | test-suite/output/Tactics.out | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/test-suite/output/Tactics.out b/test-suite/output/Tactics.out index 71c59e432..8e8b8059f 100644 --- a/test-suite/output/Tactics.out +++ b/test-suite/output/Tactics.out @@ -1 +1,4 @@ intro H; split; [ a H | e H ]. +intros; match goal with + | |- context [if ?X then _ else _] => case X + end; trivial. |