| Commit message (Collapse) | Author | Age | |
|---|---|---|---|
| * | Use r.(p) syntax to print primitive projections. |  Maxime Dénès | 2018-01-30 |
| | | | | | | | | | | | | | | There is no way today to distinguish primitive projections from compatibility constants, at least in the case of a record without parameters. We remedy to this by always using the r.(p) syntax when printing primitive projections, even with Set Printing All. The input syntax r.(p) is still elaborated to GApp, so that we can preserve the compatibility layer. Hopefully we can make up a plan to get rid of that layer, but it will require fixing a few problems. | ||
| * | [api] Move structures deprecated in the API to the core. |  Emilio Jesus Gallego Arias | 2017-11-06 |
| | | | | | We do up to `Term` which is the main bulk of the changes. | ||
| * | [general] Remove Econstr dependency from `intf` | Emilio Jesus Gallego Arias | 2017-10-25 |
| | | | | | | To this extent we factor out the relevant bits to a new file, ltac_pretype. | ||
| * | Bump year in headers. |  Pierre-Marie Pédrot | 2017-07-04 |
| | | |||
| * | Put all plugins behind an "API". |  Matej Kosik | 2017-06-07 |
 |
index : coq | |
| the Coq proof assistant |
| aboutsummaryrefslogtreecommitdiffhomepage |