diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2006-10-24 08:35:38 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2006-10-24 08:35:38 +0000 |
| commit | a0f0b0bd67899eacf916c2f9ccf8d6b29ad8bd92 (patch) | |
| tree | 206887e694924a70ca88c6996f507fe8ffcca093 /parsing/argextend.ml4 | |
| parent | f321caf5abbbadc0388fae76601745c02bff0bce (diff) | |
Hack peu élégant pour permettre de parser des listes avec séparateurs dans
TACTIC EXTEND
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9265 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'parsing/argextend.ml4')
| -rw-r--r-- | parsing/argextend.ml4 | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/parsing/argextend.ml4 b/parsing/argextend.ml4 index 07c1470c9..ebe2b2893 100644 --- a/parsing/argextend.ml4 +++ b/parsing/argextend.ml4 @@ -213,7 +213,7 @@ EXTEND [ e = argtype; LIDENT "list" -> List0ArgType e | e = argtype; LIDENT "option" -> OptArgType e ] | "0" - [ e = LIDENT -> fst (interp_entry_name loc e) + [ e = LIDENT -> fst (interp_entry_name loc e "") | "("; e = argtype; ")" -> e ] ] ; argrule: @@ -221,7 +221,9 @@ EXTEND ; genarg: [ [ e = LIDENT; "("; s = LIDENT; ")" -> - let t, g = interp_entry_name loc e in (g, Some (s,t)) + let t, g = interp_entry_name loc e "" in (g, Some (s,t)) + | e = LIDENT; "("; s = LIDENT; ","; sep = STRING; ")" -> + let t, g = interp_entry_name loc e sep in (g, Some (s,t)) | s = STRING -> if String.length s > 0 && Util.is_letter s.[0] then Pcoq.lexer.Token.using ("", s); |