coq - The formal proof system

Age	Commit message (Expand)	Author
2018-03-09	Revert "Merge PR #873: New strategy based on open scopes for deciding which n...	Maxime Dénès
2018-02-20	Refining the strategy for glueing let-ins to a sequence of binders.	Hugo Herbelin
2018-02-20	A (significant) simplification in printing notations with recursive binders.	Hugo Herbelin
2017-12-12	In printing, factorizing "match" clauses with same right-hand side.	Hugo Herbelin
2017-12-07	Merge PR #873: New strategy based on open scopes for deciding which notation ...	Maxime Dénès
2017-12-03	Adding a test for #6304 (bug with fix in notations).	Hugo Herbelin
2017-11-27	Selecting which notation to print based on current stack of scope.	Hugo Herbelin
2017-03-24	Applying same convention as in Definition for printing type in a let in.	Hugo Herbelin
2016-10-17	Fixing a few other inconsistencies with notations.	Hugo Herbelin
2016-09-14	Merge branch 'v8.5' into v8.6	Pierre-Marie Pédrot
2016-09-12	Fixing a recursive notation bug raised on coq-club on Sep 12, 2016.	Hugo Herbelin
2016-07-19	Removing a source of clash with multiple recursive patterns in notations.	Hugo Herbelin
2016-06-24	Fixing #4854 (regression introduced in 4d25b224 in relation with #4592).	Hugo Herbelin
2016-04-27	Revert "A heuristic to add parentheses in the presence of rules such as"	Hugo Herbelin
2016-04-27	A heuristic to add parentheses in the presence of rules such as	Hugo Herbelin
2016-04-19	Fixing #4677 (collision of a global variable and of a local variable	Hugo Herbelin
2014-10-21	Adapting output tests to the removal of the new token warning and to	Hugo Herbelin
2014-03-01	Never suppress the typing constraint of bound variables whose name was	Pierre-Marie Pédrot
2013-05-09	Updating some output tests in test-suite:	herbelin
2012-12-04	Revised the strategy for automatic insertion of spaces when printing	herbelin
2012-04-06	Fixing a few bugs (see #2571) related to interpretation of multiple binders	herbelin
2012-01-20	Notations with binders: Accepting using notations for functional terms	herbelin
2011-09-22	test-suite : an additional message displayed by Notation2.v	letouzey
2011-09-22	Fix test-suite for s/Defining '\1' as keyword/Identifier '\1' now a keyword/.	letouzey
2011-08-10	Partly revert commit r14389 about relaxing the condition for being a keyword	herbelin
2011-08-08	Be a bit less aggressive in declaring idents as keywords in notations	herbelin
2011-04-27	Fixing output of Notations2.v test messed up in r14060	herbelin
2011-04-25	Fixing and completing interpretation of let's in notations for iterated binders.	herbelin
2011-04-15	Take benefit of eta-expansion so that "ex P" is displayed "exists x, P x".	herbelin
2011-04-08	Fixing multiple printing bugs with "Notation f x := ..."	herbelin
2011-03-31	Did that adding a rule for printing applications as "f(x)" works.	herbelin
2010-07-22	Extension of the recursive notations mechanism	herbelin
2010-06-14	Added printing of recursive notations in cases pattern (supported by wish 2248).	herbelin
2010-04-18	Fixed some printing bugs.	herbelin
2009-04-25	- Fixing #2090 (occur check missing when trying to solve evar-evar equation).	herbelin
2009-02-06	Fixing #2044 (bad printing of primitive notation at the head of	herbelin