diff options
| author |  Guillaume Melquiond <guillaume.melquiond@inria.fr> | 2016-05-02 16:54:38 +0200 |
|---|---|---|
| committer | Guillaume Melquiond <guillaume.melquiond@inria.fr> | 2016-05-02 16:54:38 +0200 |
| commit | 857e9ff0a7927d370c8a16e723385a9b199de872 (patch) | |
| tree | 532d677db3239cf4337e909db418f8bb8d461fc6 /checker/votour.ml | |
| parent | d7a9fea94772971a52d04f9f266fe6d5e25cd40e (diff) | |
Properly handle notations containing spaces (bug #4538).
When a notation was starting or ending a space, Coq assumed the notation
had no terminal symbol in either places. Coq also considered a notation
containing only spaces to be productive. As stated in the documentation,
extraneous spaces are only meant as printing hints, they are not meant to
have any influence on parsing.
Diffstat (limited to 'checker/votour.ml')
0 files changed, 0 insertions, 0 deletions