diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2006-05-30 16:44:25 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2006-05-30 16:44:25 +0000 |
| commit | deb036a1712e802a55a6160630387fb52ce3d998 (patch) | |
| tree | b0bdd58eb37fc1254d569ee94a4c8ac6d3948643 /parsing/g_tactic.ml4 | |
| parent | 8e6dfb334bd42d58cba5a81704139afdd632df4d (diff) | |
Généralisation de with_occurrence (ex occurrence) et de red_expr pour permettre de passer les occurrences en paramètre dans ltac, par exemple à pattern
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8878 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'parsing/g_tactic.ml4')
| -rw-r--r-- | parsing/g_tactic.ml4 | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4 index dd04506ca..9a4995c03 100644 --- a/parsing/g_tactic.ml4 +++ b/parsing/g_tactic.ml4 @@ -121,8 +121,8 @@ GEXTEND Gram simple_intropattern; int_or_var: - [ [ n = integer -> Genarg.ArgArg n - | id = identref -> Genarg.ArgVar id ] ] + [ [ n = integer -> Rawterm.ArgArg n + | id = identref -> Rawterm.ArgVar id ] ] ; (* An identifier or a quotation meta-variable *) id_or_meta: @@ -155,11 +155,11 @@ GEXTEND Gram conversion: [ [ c = constr -> (None, c) | c1 = constr; "with"; c2 = constr -> (Some ([],c1), c2) - | c1 = constr; "at"; nl = LIST1 integer; "with"; c2 = constr -> + | c1 = constr; "at"; nl = LIST1 int_or_var; "with"; c2 = constr -> (Some (nl,c1), c2) ] ] ; occurrences: - [ [ "at"; nl = LIST1 integer -> nl + [ [ "at"; nl = LIST1 int_or_var -> nl | -> [] ] ] ; pattern_occ: @@ -240,7 +240,7 @@ GEXTEND Gram ] ] ; hypident_occ: - [ [ (id,l)=hypident; occs=occurrences -> (id,occs,l) ] ] + [ [ (id,l)=hypident; occs=occurrences -> ((occs,id),l) ] ] ; clause: [ [ "in"; "*"; occs=occurrences -> |