coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Workaround to fix #7731 (printing not splitting line at break hint).	Hugo Herbelin	2018-06-29
*	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
*	Adding mention of shelved/given-up status in "Show Existentials".	Hugo Herbelin	2018-02-22
*	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
*	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