coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Merge PR#713: Bump year in headers.	Maxime Dénès	2017-06-15
\|\
\| *	Bump year in headers.	Maxime Dénès	2017-06-01
* \|	Merge PR#560: Reinstate fixpoint refolding in [cbn], deactivated by mistake (...	Maxime Dénès	2017-05-31
\|\ \ \| \|/ \|/\|
* \|	Fixing a subtle bug in tclWITHHOLES.	Hugo Herbelin	2017-05-28
* \|	Fixing a bug with nested "as" clauses in "match".	Hugo Herbelin	2017-05-16
* \|	Merge PR#597: Fixing #5487 (v8.5 regression on ltac-matching expressions with...	Maxime Dénès	2017-05-02
\|\ \
* \ \	Merge PR#589: remove unneeded -emacs flag in coq-prog-args in test-suite files	Maxime Dénès	2017-05-02
\|\ \ \
* \| \| \|	Fixing Set Rewriting Schemes bugs introduced in v8.5.	Hugo Herbelin	2017-05-01
\| * \| \|	remove unneeded -emacs flag to coq-prog-args	Paul Steckler	2017-05-01
\|/ / /
\| * /	Really fixing #2602 which was wrongly working because of #5487 hiding the cause.	Hugo Herbelin	2017-05-01
\|/ /
* \|	Fix anomaly when doing [all:Check _.] during a proof.	Gaetan Gilbert	2017-04-14
\| *	Reinstate fixpoint refolding in [cbn], deactivated by mistake.	Matthieu Sozeau	2017-04-13
\|/
*	Merge branch 'origin/v8.5' into v8.6.	Hugo Herbelin	2017-04-06
\|\
* \|	Instances should obey universe binders even when defined by tactics.	Gaetan Gilbert	2017-04-03
* \|	Intern names bound in match patterns	Tej Chajed	2017-03-23
\| *	Fixing a little bug in using the "where" clause for inductive types.	Hugo Herbelin	2017-02-23
* \|	reject notations that are both 'only printing' and 'only parsing'	Ralf Jung	2017-02-16
* \|	don't require printing-only notation to be productive	Ralf Jung	2017-02-16
* \|	Fixing bugs in typing "match" (regressions #5322 and #5324 + bugs with let-ins).	Hugo Herbelin	2017-01-22
* \|	Merge remote-tracking branch 'github/pr/366' into v8.6	Maxime Dénès	2016-12-04
\|\ \
* \| \|	Fix typeclasses eauto shelving.	Théo Zimmermann	2016-11-30
\| * \|	Fix UGraph.check_eq!	Matthieu Sozeau	2016-11-30
\|/ /
* \|	Revert more of a477dc for good measure	Matthieu Sozeau	2016-11-16
* \|	Revert part of a477dc, disallow_shelved	Matthieu Sozeau	2016-11-15
* \|	Fix test-suite files relying on tcs bugs	Matthieu Sozeau	2016-11-03
* \|	typeclasses eauto Implem/doc of shelving strategy	Matthieu Sozeau	2016-11-03
* \|	Fix handling of only_classes at toplevel	Matthieu Sozeau	2016-11-03
* \|	Test new syntax for hints and typeclass options	Matthieu Sozeau	2016-11-03
* \|	Lets Hints/Instances take an optional pattern	Matthieu Sozeau	2016-11-03
* \|	Merge remote-tracking branch 'github/pr/321' into v8.6	Maxime Dénès	2016-10-28
\|\ \
* \ \	Merge branch 'v8.5' into v8.6	Pierre-Marie Pédrot	2016-10-24
\|\ \ \ \| \| \|/ \| \|/\|
* \| \|	Merge branch 'v8.5' into v8.6	Hugo Herbelin	2016-10-24
\| * \|	Fixing #3479 (parsing of "{" and "}" when a keyword starts with "{" or "}").	Hugo Herbelin	2016-10-24
\| \| *	sections/hints: prevent Not_found in get_type_of	Matthieu Sozeau	2016-10-21
\| \|/ \|/\|
* \|	Merge PR #300 into v8.6	Pierre-Marie Pédrot	2016-10-17
\|\ \
* \| \|	Example illustrating non-local inference of the default type of impossible br...	Hugo Herbelin	2016-10-17
* \| \|	Merge branch 'v8.5' into v8.6	Pierre-Marie Pédrot	2016-10-12
\|\ \ \ \| \| \|/ \| \|/\|
\| * \|	Fixing a collision about the meta-variable ".." in recursive notations.	Hugo Herbelin	2016-10-12
* \| \|	Reverting generalization and cleaning of the return clause inference in v8.6.	Hugo Herbelin	2016-10-11
* \| \|	Clean up type classes flags and update compat file.	Maxime Dénès	2016-10-05
* \| \|	fixing bug 4609: document an option governing the generation of equalities	Yves Bertot	2016-10-03
* \| \|	More tests for tactic "subst".	Hugo Herbelin	2016-10-02
\| \| *	Move vector/list compat notations to their relevant files	Jason Gross	2016-09-29
\| \|/ \|/\|
* \|	Argument : assert does fail if no arg is given (fix #4864)	Enrico Tassi	2016-09-29
* \|	Typeclass backtracking example by J. Leivant	Matthieu Sozeau	2016-09-28
* \|	Merge remote-tracking branch 'github/pr/232' into v8.6	Maxime Dénès	2016-09-28
\|\ \
* \| \|	Posssible abstractions over goal variables when inferring match return clause.	Hugo Herbelin	2016-09-26
* \| \|	Trying an abstracting dependencies heuristic for the match return clause even...	Hugo Herbelin	2016-09-26
* \| \|	Trying a no-inversion no-dependency heuristic for match return clause.	Hugo Herbelin	2016-09-26
* \| \|	Further "decide equality" tests on demand of Jason.	Hugo Herbelin	2016-09-17