diff options
| author | herbelin | 2008-04-04 14:55:47 +0000 |
|---|---|---|
| committer | herbelin | 2008-04-04 14:55:47 +0000 |
| commit | 5a4cc30c737f113a7c57d14569137b3e06f5639f (patch) | |
| tree | 2a0114f494382fc30f50ad073eaf6ec5def2daed /parsing | |
| parent | c464aab4c1aedad2ae919eb4776ced4d4d23d62a (diff) | |
Quelques améliorations des intro patterns:
- ajout de -> et <- pour substitution immédiate d'une égalité
(comportement à la subst si variable, à la rewrite in * sinon)
- ajout possibilité d'hypothèses avec paramètres
- correction d'un comportement bizarre de l'utilisation des noms dans
cas "[[|] H]" (cf CHANGES)
Ce serait bien d'avoir quelque chose comme "intros (H as <-) (H' as [ | ])"
pour décider de garder les noms, mais la syntaxe est assez
moche. Peut-être un "intros H: <- H': [ | ]" ?
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10753 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/g_tactic.ml4 | 7 |
1 files changed, 5 insertions, 2 deletions
diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4 index 64062765a0..5e50e9859d 100644 --- a/parsing/g_tactic.ml4 +++ b/parsing/g_tactic.ml4 @@ -193,6 +193,8 @@ GEXTEND Gram | prefix = pattern_ident -> IntroFresh prefix | "?" -> IntroAnonymous | id = ident -> IntroIdentifier id + | "->" -> IntroRewrite true + | "<-" -> IntroRewrite false ] ] ; simple_binding: @@ -268,14 +270,15 @@ GEXTEND Gram ; clause: [ [ "in"; "*"; occs=occurrences -> - {onhyps=None;onconcl=true;concl_occs=occs} + {onhyps=None; onconcl=true; concl_occs=occs} | "in"; "*"; "|-"; (b,occs)=concl_occ -> {onhyps=None; onconcl=b; concl_occs=occs} | "in"; hl=LIST0 hypident_occ SEP","; "|-"; (b,occs)=concl_occ -> {onhyps=Some hl; onconcl=b; concl_occs=occs} | "in"; hl=LIST0 hypident_occ SEP"," -> {onhyps=Some hl; onconcl=false; concl_occs=[]} - | -> {onhyps=Some[];onconcl=true; concl_occs=[]} ] ] + | -> + {onhyps=Some[]; onconcl=true; concl_occs=[]} ] ] ; concl_occ: [ [ "*"; occs = occurrences -> (true,occs) |