| Age | Commit message (Expand) | Author |
|---|
| 2020-11-22 | Adapting standard library, doc and test suite to ident->name renaming. | Hugo Herbelin |
| 2020-11-19 | Merge PR #12984: [printing] Order notations by matching precision first, and ... | coqbot-app[bot] |
| 2020-11-18 | In recursive notations, accept partial application over the recursive pattern. | Hugo Herbelin |
| 2020-11-17 | For printing, ordering notations by precision of the pattern. | Hugo Herbelin |
| 2020-02-11 | Fixing some residual bugs of PR #10202 (manual implicit args in subterms). | Hugo Herbelin |
| 2019-08-26 | Make kernel parametric on the lowest universe and fix #9294 | Matthieu Sozeau |
| 2019-05-23 | Fixing typos - Part 3 | JPR |
| 2019-04-29 | Revert #8187 | Vincent Laporte |
| 2018-12-19 | Put #[universes(template)] in outputs tests | Gaëtan Gilbert |
| 2018-12-04 | Selecting which notation to print based on current stack of scope. | Hugo Herbelin |
| 2018-12-04 | Pre-isolating a notation test to avoid interferences. | Hugo Herbelin |
| 2018-07-24 | Fixes #8126 (issue with notations and nested applications). | Hugo Herbelin |
| 2018-06-29 | Workaround to fix #7731 (printing not splitting line at break hint). | Hugo Herbelin |
| 2018-05-13 | Fixing a bug in printing the body of a located notation. | Hugo Herbelin |
| 2018-03-29 | Fixes #7110 ("as" untested while looking for notation for nested patterns). | Hugo Herbelin |
| 2018-03-09 | Revert "Merge PR #873: New strategy based on open scopes for deciding which n... | Maxime Dénès |
| 2018-02-20 | Trying a hack to support {'pat|P} without breaking compatibility. | Hugo Herbelin |
| 2018-02-20 | Adding notations of the form "{'pat|P}", "exists2 'pat, P & Q", etc. | Hugo Herbelin |
| 2018-02-20 | Change default for notations with variables bound to both terms and binders. | Hugo Herbelin |
| 2018-02-20 | Notations: Adding modifiers to tell which kind of binder a constr can parse. | Hugo Herbelin |
| 2018-02-20 | When printing a notation with "match", more flexibility in matching equations. | Hugo Herbelin |
| 2018-02-20 | Adding general support for irrefutable disjunctive patterns. | Hugo Herbelin |
| 2018-02-20 | Using an "as" clause when needed for printing irrefutable patterns. | Hugo Herbelin |
| 2018-02-20 | A (significant) simplification in printing notations with recursive binders. | Hugo Herbelin |
| 2018-02-20 | Respecting the ident/pattern distinction in notation modifiers. | Hugo Herbelin |
| 2018-02-20 | Adding support for parsing subterms of a notation as "pattern". | Hugo Herbelin |
| 2018-02-20 | Adding patterns in the category of binders for notations. | Hugo Herbelin |
| 2018-02-20 | In printing notations with "match", reasoning up to the order of clauses. | Hugo Herbelin |
| 2018-02-20 | Supporting recursive notations reversing the left-to-right order. | Hugo Herbelin |
| 2018-02-20 | Allowing variables used in recursive notation to occur several times in pattern. | Hugo Herbelin |
| 2018-02-20 | Allows recursive patterns for binders to be associative on the left. | Hugo Herbelin |
| 2018-02-20 | Fixing/improving notations with recursive patterns. | Hugo Herbelin |
| 2018-02-20 | Adding support for re-folding notation referring to isolated "forall '(x,y), t". | Hugo Herbelin |
| 2017-11-27 | Selecting which notation to print based on current stack of scope. | Hugo Herbelin |
| 2017-11-27 | Pre-isolating a notation test to avoid interferences. | Hugo Herbelin |
| 2017-09-25 | BZ#5739, Allow level for leftmost nonterminal for printing-ony Notations | Paul Steckler |
| 2017-09-12 | Fixing a bug of recursive notations introduced in dfdaf4de. | Hugo Herbelin |
| 2017-08-29 | Adding a test for #5569 (warning about skipping spaces). | Hugo Herbelin |
| 2017-08-29 | A little reorganization of notations + a fix to #5608. | Hugo Herbelin |
| 2017-07-26 | Adding support for recursive notations of the form "x , .. , y , z". | Hugo Herbelin |
| 2017-06-08 | Merge branch 'v8.6' | Pierre-Marie Pédrot |
| 2017-05-31 | Fixing a too lax constraint for finding recursive binder part of a notation. | Hugo Herbelin |
| 2017-05-20 | Added a test for #4765 (an example of printing abbreviation with binders). | Hugo Herbelin |
| 2017-05-17 | Fixing bug #5526,allow nonlinear variables in Notation patterns | Paul Steckler |
| 2016-07-19 | Taking into account binding patterns when agglutinating sequences of binders. | Hugo Herbelin |
| 2016-07-19 | Notations: fixing multiple binders used as terms in reverse order. | Hugo Herbelin |
| 2016-07-18 | A new step on using alpha-conversion in printing notations. | Hugo Herbelin |
| 2016-07-17 | 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 | Fixing a bug in recognizing a recursive pattern of notations | Hugo Herbelin |
