aboutsummaryrefslogtreecommitdiff
path: root/test-suite/output/Notations4.v
AgeCommit message (Expand)Author
2020-05-13Extending support for mixing binders and terms in abbreviations.Hugo Herbelin
2020-04-11If a custom entry has global, a bound variable is valid in this entry.Hugo Herbelin
2020-04-11If a custom entry has global, an argument-free abbreviation is valid in this ...Hugo Herbelin
2020-02-20Merge PR #10832: Addressing #6082 and #7766: warning when overriding notation...Emilio Jesus Gallego Arias
2020-02-19Revert "Granting #9516 and #9518 (support for numerals and strings in custom ...Hugo Herbelin
2020-02-19Addressing #6082 and #7766 (overriding format of notation).Hugo Herbelin
2020-02-16Revert "Suite picking numeral notation"Hugo Herbelin
2020-02-16Suite picking numeral notationHugo Herbelin
2020-02-16Granting #9516 and #9518 (support for numerals and strings in custom entries).Hugo Herbelin
2020-02-15Fixes #11331 (unexpected level collisions between custom entries and constr).Hugo Herbelin
2020-01-31More tolerant in format for recursive notations.Hugo Herbelin
2019-12-03Printing: Interleaving search for notations and removal of coercions.Hugo Herbelin
2019-11-21A refined version of #8890 which prevents #11033.Hugo Herbelin
2019-11-11Miscellaneous improvements of the syntax of records.Hugo Herbelin
2019-05-10Use Print Custom Grammar to inspect custom entriesJasper Hugunin
2019-04-29Revert #8187Vincent Laporte
2019-04-29Revert #9249Vincent Laporte
2019-02-19Notations: Fixing a printing bug with patterns.Hugo Herbelin
2019-02-04Primitive integersMaxime Dénès
2019-01-25Notations: Removing useless parentheses on abbrevs for prefix of an application.Hugo Herbelin
2018-12-25Fixing printing bug due to using equality ill-checking hash key of kernel name.Hugo Herbelin
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-27 02:35:50 +0000