| Commit message (Collapse) | Author | Age | |
|---|---|---|---|
| * | Move vector/list compat notations to their relevant files |  Jason Gross | 2016-09-29 |
| | | | | | | | | Since edb55a94fc5c0473e57f5a61c0c723194c2ff414 landed, compat notations no longer modify the parser in non-compat-mode, so we can do this without breaking Ltac parsing. Also update the related test-suite files. | ||
| * | Unbreak singleton list-like notation (-compat 8.4) | Jason Gross | 2016-06-09 |
| With this commit, it is possible to write notations so that singleton lists are usable in both 8.4 and 8.5pl1 -compat. Longer lists await the ability to remove notations from the parser. | |||
 |
index : coq | |
| the Coq proof assistant |
| aboutsummaryrefslogtreecommitdiffhomepage |