| Commit message (Collapse) | Author | Age | |
|---|---|---|---|
| * | Properly handle notations containing spaces (bug #4538). |  Guillaume Melquiond | 2016-05-02 |
| 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. | |||
 |
index : coq | |
| the Coq proof assistant |
| aboutsummaryrefslogtreecommitdiffhomepage |