| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2017-06-14 | Remove support for Coq 8.4. | Guillaume Melquiond | |
| 2017-05-01 | remove unneeded -emacs flag to coq-prog-args | Paul Steckler | |
| 2016-09-29 | Move vector/list compat notations to their relevant files | Jason Gross | |
| 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. | |||
| 2016-06-09 | Unbreak singleton list-like notation (-compat 8.4) | Jason Gross | |
| 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 formal proof system |
| aboutsummaryrefslogtreecommitdiff |