aboutsummaryrefslogtreecommitdiff
path: root/test-suite/output/Notations2.v
AgeCommit message (Expand)Author
2020-11-22Adapting standard library, doc and test suite to ident->name renaming.Hugo Herbelin
2019-04-29Revert #8187Vincent Laporte
2018-12-04Selecting which notation to print based on current stack of scope.Hugo Herbelin
2018-03-09Revert "Merge PR #873: New strategy based on open scopes for deciding which n...Maxime Dénès
2018-02-20A (significant) simplification in printing notations with recursive binders.Hugo Herbelin
2017-12-12In printing, factorizing "match" clauses with same right-hand side.Hugo Herbelin
2017-12-07Merge PR #873: New strategy based on open scopes for deciding which notation ...Maxime Dénès
2017-12-03Adding a test for #6304 (bug with fix in notations).Hugo Herbelin
2017-11-27Selecting which notation to print based on current stack of scope.Hugo Herbelin
2016-10-17Fixing a few other inconsistencies with notations.Hugo Herbelin
2016-09-14Merge branch 'v8.5' into v8.6Pierre-Marie Pédrot
2016-09-12Fixing a recursive notation bug raised on coq-club on Sep 12, 2016.Hugo Herbelin
2016-06-24Fixing #4854 (regression introduced in 4d25b224 in relation with #4592).Hugo Herbelin
2016-04-27Revert "A heuristic to add parentheses in the presence of rules such as"Hugo Herbelin
2016-04-27A heuristic to add parentheses in the presence of rules such asHugo Herbelin
2016-04-22Fixing output test Notations2.Hugo Herbelin
2016-04-19Fixing #4677 (collision of a global variable and of a local variableHugo Herbelin
2012-04-06Fixing a few bugs (see #2571) related to interpretation of multiple bindersherbelin
2012-01-20Notations with binders: Accepting using notations for functional termsherbelin
2011-04-25Fixing and completing interpretation of let's in notations for iterated binders.herbelin
2011-04-15Take benefit of eta-expansion so that "ex P" is displayed "exists x, P x".herbelin
2011-04-08Fixing multiple printing bugs with "Notation f x := ..."herbelin
2011-03-31Did that adding a rule for printing applications as "f(x)" works.herbelin
2011-03-16Remove some weird syntax "fun ... ," that used to be accepted (cf r13876)letouzey
2010-07-22Extension of the recursive notations mechanismherbelin
2010-06-14Added printing of recursive notations in cases pattern (supported by wish 2248).herbelin
2010-04-18Fixed some printing bugs.herbelin
2009-04-25- Fixing #2090 (occur check missing when trying to solve evar-evar equation).herbelin
2009-02-06Fixing #2044 (bad printing of primitive notation at the head ofherbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 15:43:38 +0000