| Commit message (Collapse) | Author | Age | |
|---|---|---|---|
| * | Taking into account binding patterns when agglutinating sequences of binders. |  Hugo Herbelin | 2016-07-19 |
| | | | | | | Supporting accordingly printing of sequences of binders including binding patterns. | ||
| * | 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 |
| | | | | | | | | A couple of bugs have been found. Example #4932 is now printing correctly in the presence of multiple binders (when no let-in, no irrefutable patterns). | ||
| * | 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 |
| | | | | | | | | | | | | | | Further work would include: - Identify binders up to alpha-conversion (see #4932 with a list of binders of length at least 2, or #4592 on printing notations such as ex2). A cool example that one could also consider supporting: - Notation "[[ a , .. , b | .. | a , .. , b ]]" := (cons (cons a .. (cons b nil) ..) .. (cons a .. (cons b nil) ..) ..). | ||
| * | Fixing a bug in recognizing a recursive pattern of notations | Hugo Herbelin | 2016-07-17 |
| | | | | | immediately in the scope of another recursive pattern. | ||
| * | 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 |