coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Introduce an option to allow nested lemma, and turn it off by default.	Théo Zimmermann	2018-05-17
*	[ssr] import ssreflect test suite from math-comp	Enrico Tassi	2018-05-15
*	Fixing a bug in printing the body of a located notation.	Hugo Herbelin	2018-05-13
*	Making explicit that errors happen in one of five executation phases.	Hugo Herbelin	2018-05-02
*	Merge PR #7116: Fixes #7110: missing test on the absence of a "as" while look...	Emilio Jesus Gallego Arias	2018-04-09
\|\
* \	Merge PR #7165: [ssr] check cleared hyps do exist (fix #7050)	Maxime Dénès	2018-04-09
\|\ \
* \ \	Merge PR #7127: Fix #6257: anomaly with Printing Projections and Context.	Hugo Herbelin	2018-04-04
\|\ \ \
\| \| * \|	ssr: check cleared hyps do exist (fix #7050)	Enrico Tassi	2018-04-04
* \| \| \|	Fix #6404 - Print tactics called by ML tactics	Jason Gross	2018-04-02
\| \|/ / \|/\| \|
\| * \|	Fix #6257: anomaly with Printing Projections and Context.	Gaëtan Gilbert	2018-03-30
\|/ /
\| *	Fixes #7110 ("as" untested while looking for notation for nested patterns).	Hugo Herbelin	2018-03-29
* \|	Slightly refining some error messages about unresolvable evars.	Hugo Herbelin	2018-03-24
\|/
*	Revert "Merge PR #873: New strategy based on open scopes for deciding which n...	Maxime Dénès	2018-03-09
*	Merge PR #6895: [compat] Remove "Refolding Reduction" option.	Maxime Dénès	2018-03-09
\|\
* \	Merge PR #6945: Fix error with univ binders on monomorphic records.	Maxime Dénès	2018-03-09
\|\ \
* \ \	Merge PR #6816: Adding mention of shelved/given-up status in Show Existentials	Maxime Dénès	2018-03-08
\|\ \ \
\| \| \| *	[compat] Remove "Refolding Reduction" option.	Emilio Jesus Gallego Arias	2018-03-08
\| \|_\|/ \|/\| \|
\| \| *	Fix error with univ binders on monomorphic records.	Gaëtan Gilbert	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
\|/ /