| Commit message (Expand) | Author | Age | |
|---|---|---|---|
| * | Added a test for #4765 (an example of printing abbreviation with binders). |  Hugo Herbelin | 2017-05-20 |
| * | Taking into account binding patterns when agglutinating sequences of binders. | Hugo Herbelin | 2016-07-19 |
| * | Notations: fixing multiple binders used as terms in reverse order. | Hugo Herbelin | 2016-07-19 |
| * | A new step on using alpha-conversion in printing notations. | Hugo Herbelin | 2016-07-18 |
| * | Partial fix to #4592 (notation requiring alpha-conversion for printing). | Hugo Herbelin | 2016-07-17 |
| * | More examples of recursive notations, with emphasis in reference manual. | Hugo Herbelin | 2016-07-17 |
| * | Fixing a bug in recognizing a recursive pattern of notations | Hugo Herbelin | 2016-07-17 |
| * | Fixing interpretation of notations w/ opposite instances of a recursive pattern. | Hugo Herbelin | 2016-07-17 |
| * | Fixing printing of notations with several instances of a recursive pattern. | Hugo Herbelin | 2016-07-17 |
 |
index : coq | |
| the Coq proof assistant |
| aboutsummaryrefslogtreecommitdiffhomepage |