aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/output/Notations2.v
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
* 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
|/
* 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
* | 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 output test Notations2.Gravatar Hugo Herbelin2016-04-22
* Fixing #4677 (collision of a global variable and of a local variableGravatar Hugo Herbelin2016-04-19
* 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
* 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
* Remove some weird syntax "fun ... ," that used to be accepted (cf r13876)Gravatar letouzey2011-03-16
* 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-26 17:52:04 +0000