| Commit message (Expand) | Author | Age |
* | Fixing a bug in printing the body of a located notation. | Hugo Herbelin | 2018-05-13 |
* | Fixes #7110 ("as" untested while looking for notation for nested patterns). | Hugo Herbelin | 2018-03-29 |
* | Revert "Merge PR #873: New strategy based on open scopes for deciding which n... | Maxime Dénès | 2018-03-09 |
* | 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 | 2018-02-20 |
* | 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-11-27 |
* | BZ#5739, Allow level for leftmost nonterminal for printing-ony Notations | Paul Steckler | 2017-09-25 |
* | Fixing a bug of recursive notations introduced in dfdaf4de. | Hugo Herbelin | 2017-09-12 |
* | 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-08-29 |
* | Adding support for recursive notations of the form "x , .. , y , z". | Hugo Herbelin | 2017-07-26 |
* | Merge branch 'v8.6' | Pierre-Marie Pédrot | 2017-06-08 |
|\ |
|
* | | Fixing a too lax constraint for finding recursive binder part of a notation. | Hugo Herbelin | 2017-05-31 |
* | | Added a test for #4765 (an example of printing abbreviation with binders). | Hugo Herbelin | 2017-05-20 |
| * | Fixing bug #5526,allow nonlinear variables in Notation patterns | Paul Steckler | 2017-05-17 |
|/ |
|
* | 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-19 |
* | A new step on using alpha-conversion in printing notations. | Hugo Herbelin | 2016-07-18 |
* | 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 | 2016-07-17 |
* | Fixing interpretation of notations w/ opposite instances of a recursive pattern. | Hugo Herbelin | 2016-07-17 |
* | Fixing printing of notations with several instances of a recursive pattern. | Hugo Herbelin | 2016-07-17 |