aboutsummaryrefslogtreecommitdiff
path: root/test-suite/output/Notations4.v
AgeCommit message (Expand)Author
2021-02-26Signed primitive integersAna
2020-11-24Merge PR #13436: Fixes #13432: typo in #11172 causing notations mentioning a ...coqbot-app[bot]
2020-11-22Adapting standard library, doc and test suite to ident->name renaming.Hugo Herbelin
2020-11-21Fixes #13432: regression with notations involving coercions caused by #11172.Hugo Herbelin
2020-11-20Tests for notations with general single (non-recursive) binders.Hugo Herbelin
2020-11-17For printing, ordering notations by precision of the pattern.Hugo Herbelin
2020-11-05Regression tests for the various combinations of mixed terms and binders in n...Hugo Herbelin
2020-10-30Renaming Numeral.v into Number.vPierre Roux
2020-09-11Rename Numeral Notation command to Number NotationPierre Roux
2020-08-09Fixing a coercion entry transitivity bug.Hugo Herbelin
2020-07-15Fix bug #12691 (an only parsing notation induces a generic printing format).Hugo Herbelin
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-01-31 12:40:19 +0000