diff options
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 |