diff options
| author | amahboub | 2008-10-30 22:16:34 +0000 |
|---|---|---|
| committer | amahboub | 2008-10-30 22:16:34 +0000 |
| commit | 8f2e16b7ef5178ff89a57adca2a3223407a256d6 (patch) | |
| tree | 65616a140dc1cdc5c4475a9233cdd93a5c1f8802 /interp/implicit_quantifiers.ml | |
| 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 'interp/implicit_quantifiers.ml')
0 files changed, 0 insertions, 0 deletions