diff options
| author |  filliatr <filliatr@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-01-30 09:19:30 +0000 |
|---|---|---|
| committer | filliatr <filliatr@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-01-30 09:19:30 +0000 |
| commit | 0577c06262f89785b41f110840a1646c7981fe12 (patch) | |
| tree | 46b8bb51c71429b0a2c3710d842af4186bc410ce /parsing/pcoq.ml4 | |
| parent | 3378c2cc6a403e78f3fd800dcaca67a82bfb9b4d (diff) | |
backtrack sur le lexeur de la V6
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1289 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'parsing/pcoq.ml4')
| -rw-r--r-- | parsing/pcoq.ml4 | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/parsing/pcoq.ml4 b/parsing/pcoq.ml4 index 968a4cba4..5776cb811 100644 --- a/parsing/pcoq.ml4 +++ b/parsing/pcoq.ml4 @@ -7,8 +7,8 @@ open Util (* The lexer of Coq *) (* Note: removing a token. - We do nothing because remove_token is called only when removing a grammar - rule with Grammar.delete_rule. The latter command is called only when + We do nothing because [remove_token] is called only when removing a grammar + rule with [Grammar.delete_rule]. The latter command is called only when unfreezing the state of the grammar entries (see GRAMMAR summary, file env/metasyntax.ml). Therefore, instead of removing tokens one by one, we unfreeze the state of the lexer. This restores the behaviour of the |