coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Merge PR #6816: Adding mention of shelved/given-up status in Show Existentials	Maxime Dénès	2018-03-08
\|\
* \	Merge PR #6791: Removing compatibility support for versions older than 8.5.	Maxime Dénès	2018-03-04
\|\ \
\| * \|	Turn warning for deprecated notations on.	Théo Zimmermann	2018-03-02
* \| \|	[test-suite] Add a basic test-case for `Load`.	Emilio Jesus Gallego Arias	2018-02-28
\|/ /
* \|	Merge PR #6823: Fixes #6821 (bug in protecting notation printing from infinit...	Maxime Dénès	2018-02-28
\|\ \
* \ \	Merge PR #6599: Decimals in prelude	Maxime Dénès	2018-02-24
\|\ \ \
\| \| * \|	Fixes #6821 (bug in protecting notation printing from infinite eta-expansion).	Hugo Herbelin	2018-02-23
\| \|/ / \|/\| \|
\| \| *	Adding mention of shelved/given-up status in "Show Existentials".	Hugo Herbelin	2018-02-22
\| \|/ \|/\|
\| *	Update SearchPattern.out for numeral notations	Jason Gross	2018-02-20
* \|	Trying a hack to support {'pat\|P} without breaking compatibility.	Hugo Herbelin	2018-02-20
* \|	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
* \|	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	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
* \|	Using name given by user to name a 'pat, if any.	Hugo Herbelin	2018-02-20
* \|	Moving the argument of CProdN/CLambdaN from binder_expr to local_binder_expr.	Hugo Herbelin	2018-02-20
* \|	Adding support for re-folding notation referring to isolated "forall '(x,y), t".	Hugo Herbelin	2018-02-20
\|/
*	Merge PR #1082: Fixing Print for inductive types with let-in in parameters	Maxime Dénès	2018-02-12
\|\
* \	Merge PR #6418: More detailed error messages for Canonical Structure, #6398	Maxime Dénès	2018-02-12
\|\ \
\| * \|	More detailed error messages for Canonical Structure, #6398	Paul Steckler	2018-02-06
* \| \|	Use r.(p) syntax to print primitive projections.	Maxime Dénès	2018-01-30
\|/ /
* \|	add optimize_heap tactic for #6488	Paul Steckler	2018-01-03
* \|	Merge PR #6234: Make the micromega extraction check a regular output test.	Maxime Dénès	2017-12-20
\|\ \
* \| \|	Make [abstract] nodes show up in the Ltac profile	Jason Gross	2017-12-14
* \| \|	Merge PR #6386: Catch errors while coercing 'and' intro patterns	Maxime Dénès	2017-12-14
\|\ \ \
\| \| \| *	Fixing a bug of Print for inductive types with let-ins in parameters.	Hugo Herbelin	2017-12-14
* \| \| \|	In printing, factorizing "match" clauses with same right-hand side.	Hugo Herbelin	2017-12-12
\| \|_\|/ \|/\| \|
\| * \|	Catch errors while coercing 'and' intro patterns	Tej Chajed	2017-12-11
\|/ /
* \|	Merge PR #6158: Allows a level in the raw and glob printers	Maxime Dénès	2017-12-08
\|\ \
* \ \	Merge PR #873: New strategy based on open scopes for deciding which notation ...	Maxime Dénès	2017-12-07
\|\ \ \
* \ \ \	Merge PR #890: Global universe declarations	Maxime Dénès	2017-12-05
\|\ \ \ \
* \ \ \ \	Merge PR #6306: Adding a test for #6304 (a bug with "fix" in notations).	Maxime Dénès	2017-12-05
\|\ \ \ \ \
* \ \ \ \ \	Merge PR #6220: Use OCaml criteria for infix ops in extraction, #6212	Maxime Dénès	2017-12-05
\|\ \ \ \ \ \
* \ \ \ \ \ \	Merge PR #6210: More complete not-fully-applied error messages, #6145	Maxime Dénès	2017-12-05
\|\ \ \ \ \ \ \
\| \| \| * \| \| \| \|	Adding a test for #6304 (bug with fix in notations).	Hugo Herbelin	2017-12-03
\| \|_\|/ / / / / \|/\| \| \| \| \| \|
\| \| \| * \| \| \|	Cleanup API for registering universe binders.	Matthieu Sozeau	2017-12-01
\| \|_\|/ / / / \|/\| \| \| \| \|
\| * \| \| \| \|	more complete not-fully-applied error messages, #6145	Paul Steckler	2017-11-28
\| \| \| \| \| *	Make the micromega extraction check a regular output test.	Gaëtan Gilbert	2017-11-28
\| \|_\|_\|_\|/ \|/\| \| \| \|