aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/output/Notations3.v
Commit message (Expand)AuthorAge
* Taking into account binding patterns when agglutinating sequences of binders.Gravatar Hugo Herbelin2016-07-19
* Notations: fixing multiple binders used as terms in reverse order.Gravatar Hugo Herbelin2016-07-19
* A new step on using alpha-conversion in printing notations.Gravatar Hugo Herbelin2016-07-18
* Partial fix to #4592 (notation requiring alpha-conversion for printing).Gravatar Hugo Herbelin2016-07-17
* More examples of recursive notations, with emphasis in reference manual.Gravatar Hugo Herbelin2016-07-17
* Fixing a bug in recognizing a recursive pattern of notationsGravatar Hugo Herbelin2016-07-17
* Fixing interpretation of notations w/ opposite instances of a recursive pattern.Gravatar Hugo Herbelin2016-07-17
* Fixing printing of notations with several instances of a recursive pattern.Gravatar Hugo Herbelin2016-07-17