diff options
| author | msozeau | 2008-04-20 18:18:49 +0000 |
|---|---|---|
| committer | msozeau | 2008-04-20 18:18:49 +0000 |
| commit | c82f88f9dd833dc33dacfe03822bc5987041e6ac (patch) | |
| tree | 82fe1e45454eefa27e471ecdf501072243893e15 /parsing | |
| parent | 25c9cfe773f69669c867802f6c433b6250ceaf9b (diff) | |
Work on the "occurrences" tactic argument. It is now possible to pass
lists of occurrences through tactics. Implement the "at" variants of
setoid_replace correspondingly.
Fix in class_tactics efor w_unify not checking types when unifying a
meta with anything (problematic at top-level only).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10820 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/g_tactic.ml4 | 14 |
1 files changed, 7 insertions, 7 deletions
diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4 index 28c2acb811..b6a3c985a0 100644 --- a/parsing/g_tactic.ml4 +++ b/parsing/g_tactic.ml4 @@ -166,15 +166,15 @@ GEXTEND Gram [ [ c = global -> AN c | s = ne_string -> ByNotation (loc,s) ] ] ; - occurrences: + occs: [ [ "at"; nl = LIST1 int_or_var -> nl | -> [] ] ] ; pattern_occ: - [ [ c = constr; nl = occurrences -> (nl,c) ] ] + [ [ c = constr; nl = occs -> (nl,c) ] ] ; unfold_occ: - [ [ c = smart_global; nl = occurrences -> (nl,c) ] ] + [ [ c = smart_global; nl = occs -> (nl,c) ] ] ; intropatterns: [ [ l = LIST0 simple_intropattern -> l ]] @@ -266,10 +266,10 @@ GEXTEND Gram ] ] ; hypident_occ: - [ [ (id,l)=hypident; occs=occurrences -> ((occs,id),l) ] ] + [ [ (id,l)=hypident; occs=occs -> ((occs,id),l) ] ] ; clause: - [ [ "in"; "*"; occs=occurrences -> + [ [ "in"; "*"; occs=occs -> {onhyps=None; onconcl=true; concl_occs=occs} | "in"; "*"; "|-"; (b,occs)=concl_occ -> {onhyps=None; onconcl=b; concl_occs=occs} @@ -277,13 +277,13 @@ GEXTEND Gram {onhyps=Some hl; onconcl=b; concl_occs=occs} | "in"; hl=LIST0 hypident_occ SEP"," -> {onhyps=Some hl; onconcl=false; concl_occs=[]} - | occs=occurrences -> + | occs=occs -> {onhyps=Some[]; onconcl=true; concl_occs=occs} | -> {onhyps=Some[]; onconcl=true; concl_occs=[]} ] ] ; concl_occ: - [ [ "*"; occs = occurrences -> (true,occs) + [ [ "*"; occs = occs -> (true,occs) | -> (false, []) ] ] ; simple_clause: |