| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2020-05-27 | Release notes for 8.12. | Théo Zimmermann | |
| 2020-01-22 | Add explicit types to changelog entries. | Théo Zimmermann | |
| 2020-01-22 | Fix typo in changelog entry. | Théo Zimmermann | |
| 2019-12-03 | Update ↵ | Hugo Herbelin | |
| doc/changelog/03-notations/11172-master+coercion-notation-interleaved-printing.rst Co-Authored-By: Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr> | |||
| 2019-12-03 | Printing: Interleaving search for notations and removal of coercions. | Hugo Herbelin | |
| We renounce to the ad hoc rule preferring a notation w/o delimiter for a term with coercions stripped over a notation for the fully-applied terms with coercions not removed. Instead, we interleave removal of coercions and search for notations: we prefer a notation for the fully applied term, and, if not, try to remove one coercion, and try again a notation for the remaining term, and if not, try to remove the next coercion, etc. Note: the flatten_application could be removed if prim_token were able to apply on a prefix of an application node. | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |