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 /pretyping/pattern.mli | |
| 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 'pretyping/pattern.mli')
| -rw-r--r-- | pretyping/pattern.mli | 7 |
1 files changed, 5 insertions, 2 deletions
diff --git a/pretyping/pattern.mli b/pretyping/pattern.mli index 0815f8721..4093f5e11 100644 --- a/pretyping/pattern.mli +++ b/pretyping/pattern.mli @@ -39,8 +39,9 @@ type constr_pattern = | PLetIn of name * constr_pattern * constr_pattern | PSort of rawsort | PMeta of patvar option - | PCase of (inductive option * case_style) - * constr_pattern option * constr_pattern * constr_pattern array + | PIf of constr_pattern * constr_pattern * constr_pattern + | PCase of (case_style * int array * inductive option * int option) + * constr_pattern * constr_pattern * constr_pattern array | PFix of fixpoint | PCoFix of cofixpoint @@ -76,3 +77,5 @@ val pattern_of_rawconstr : rawconstr -> val instantiate_pattern : (identifier * constr_pattern) list -> constr_pattern -> constr_pattern + +val lift_pattern : int -> constr_pattern -> constr_pattern |