aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/output/Notations2.out
Commit message (Expand)AuthorAge
* Revert "Merge PR #873: New strategy based on open scopes for deciding which n...Gravatar Maxime Dénès2018-03-09
* Refining the strategy for glueing let-ins to a sequence of binders.Gravatar Hugo Herbelin2018-02-20
* A (significant) simplification in printing notations with recursive binders.Gravatar Hugo Herbelin2018-02-20
* In printing, factorizing "match" clauses with same right-hand side.Gravatar Hugo Herbelin2017-12-12
* Merge PR #873: New strategy based on open scopes for deciding which notation ...Gravatar Maxime Dénès2017-12-07
|\
* | Adding a test for #6304 (bug with fix in notations).Gravatar Hugo Herbelin2017-12-03
| * Selecting which notation to print based on current stack of scope.Gravatar Hugo Herbelin2017-11-27
|/
* Applying same convention as in Definition for printing type in a let in.Gravatar Hugo Herbelin2017-03-24
* Fixing a few other inconsistencies with notations.Gravatar Hugo Herbelin2016-10-17
* Merge branch 'v8.5' into v8.6Gravatar Pierre-Marie Pédrot2016-09-14
|\
| * Fixing a recursive notation bug raised on coq-club on Sep 12, 2016.Gravatar Hugo Herbelin2016-09-12
* | Removing a source of clash with multiple recursive patterns in notations.Gravatar Hugo Herbelin2016-07-19
* | Fixing #4854 (regression introduced in 4d25b224 in relation with #4592).Gravatar Hugo Herbelin2016-06-24
* | Revert "A heuristic to add parentheses in the presence of rules such as"Gravatar Hugo Herbelin2016-04-27
* | A heuristic to add parentheses in the presence of rules such asGravatar Hugo Herbelin2016-04-27
|/
* Fixing #4677 (collision of a global variable and of a local variableGravatar Hugo Herbelin2016-04-19
* Adapting output tests to the removal of the new token warning and toGravatar Hugo Herbelin2014-10-21
* Never suppress the typing constraint of bound variables whose name wasGravatar Pierre-Marie Pédrot2014-03-01
* Updating some output tests in test-suite:Gravatar herbelin2013-05-09
* Revised the strategy for automatic insertion of spaces when printingGravatar herbelin2012-12-04
* Fixing a few bugs (see #2571) related to interpretation of multiple bindersGravatar herbelin2012-04-06
* Notations with binders: Accepting using notations for functional termsGravatar herbelin2012-01-20
* test-suite : an additional message displayed by Notation2.vGravatar letouzey2011-09-22
* Fix test-suite for s/Defining '\1' as keyword/Identifier '\1' now a keyword/.Gravatar letouzey2011-09-22
* Partly revert commit r14389 about relaxing the condition for being a keywordGravatar herbelin2011-08-10
* Be a bit less aggressive in declaring idents as keywords in notationsGravatar herbelin2011-08-08
* Fixing output of Notations2.v test messed up in r14060Gravatar herbelin2011-04-27
* Fixing and completing interpretation of let's in notations for iterated binders.Gravatar herbelin2011-04-25
* Take benefit of eta-expansion so that "ex P" is displayed "exists x, P x".Gravatar herbelin2011-04-15
* Fixing multiple printing bugs with "Notation f x := ..."Gravatar herbelin2011-04-08
* Did that adding a rule for printing applications as "f(x)" works.Gravatar herbelin2011-03-31
* Extension of the recursive notations mechanismGravatar herbelin2010-07-22
* Added printing of recursive notations in cases pattern (supported by wish 2248).Gravatar herbelin2010-06-14
* Fixed some printing bugs.Gravatar herbelin2010-04-18
* - Fixing #2090 (occur check missing when trying to solve evar-evar equation).Gravatar herbelin2009-04-25
* Fixing #2044 (bad printing of primitive notation at the head ofGravatar herbelin2009-02-06
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-19 02:24:31 +0000