aboutsummaryrefslogtreecommitdiff
path: root/test-suite/output/Notations4.v
AgeCommit message (Expand)Author
2018-12-04Giving to type_scope a softer role in printing.Hugo Herbelin
2018-12-04Printing priority to most recent notation in case of non-open scopes with delim.Hugo Herbelin
2018-12-04Using scope for printing: more tests.Hugo Herbelin
2018-12-04Fixing #8551 (missing delimiters when notation exists both lonely and in scope).Hugo Herbelin
2018-12-04Selecting which notation to print based on current stack of scope.Hugo Herbelin
2018-11-20Notations: Trying using a notation with or w/o removal of coercions.Hugo Herbelin
2018-10-31Notations: fixing a bug with abbreviations in custom entries.Hugo Herbelin
2018-07-29Adding support for custom entries in notations.Hugo Herbelin