diff options
| author |  amahboub <amahboub@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-10-30 22:16:34 +0000 |
|---|---|---|
| committer | amahboub <amahboub@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-10-30 22:16:34 +0000 |
| commit | 8f2e16b7ef5178ff89a57adca2a3223407a256d6 (patch) | |
| tree | 65616a140dc1cdc5c4475a9233cdd93a5c1f8802 /parsing/g_prim.ml4 | |
| parent | 1f50d34daf979b8b5ea0c782b259b83b3f6d7a42 (diff) | |
The lexer is changer to break former PATTERNIDENT into two tokens.
This allows more flexibility in the other uses of the question mark
and in particular suppresses the hack for rewriter in g_tactic.ml4
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11524 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'parsing/g_prim.ml4')
| -rw-r--r-- | parsing/g_prim.ml4 | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/parsing/g_prim.ml4 b/parsing/g_prim.ml4 index c24534e2d..524e7b468 100644 --- a/parsing/g_prim.ml4 +++ b/parsing/g_prim.ml4 @@ -45,7 +45,7 @@ GEXTEND Gram [ [ s = IDENT -> id_of_string s ] ] ; pattern_ident: - [ [ s = PATTERNIDENT -> id_of_string s ] ] + [ [ s = LEFTQMARK; id = ident -> id ] ] ; pattern_identref: [ [ id = pattern_ident -> (loc, id) ] ] |