coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Merge PR#713: Bump year in headers.	Maxime Dénès	2017-06-15
\|\
* \	Merge PR#440: Univs: fix bug #5365, generation of u+k <= v constraints	Maxime Dénès	2017-06-15
\|\ \
\| * \|	Univs: fix bug #5365, generation of u+k <= v constraints	Matthieu Sozeau	2017-06-05
\| \| *	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
\|\ \ \ \| \|_\|/ \|/\| \|
* \| \|	Merge PR#546: Fix for bug #4499 and other minor related bugs	Maxime Dénès	2017-05-29
\|\ \ \
* \| \| \|	fix swapping of ids in tuples, bug 5486	Paul Steckler	2017-05-17
* \| \| \|	Removing a line warned unused.	Hugo Herbelin	2017-05-14
* \| \| \|	Fixing #5487 (v8.5 regression on ltac-matching expressions with evars).	Hugo Herbelin	2017-05-01
* \| \| \|	Really fixing #2602 which was wrongly working because of #5487 hiding the cause.	Hugo Herbelin	2017-05-01
* \| \| \|	Revert "Fixing #5487 (v8.5 regression on ltac-matching expressions with evars)."	Maxime Dénès	2017-04-28
* \| \| \|	Fixing #5487 (v8.5 regression on ltac-matching expressions with evars).	Hugo Herbelin	2017-04-28
* \| \| \|	Fix bug #5377: @? patterns broken.	Pierre-Marie Pédrot	2017-04-20
\| \| * \|	Reinstate fixpoint refolding in [cbn], deactivated by mistake.	Matthieu Sozeau	2017-04-13
\| \|/ / \|/\| \|
* \| \|	Fixing #5460 (limitation in computing deps in pattern-matching compilation).	Hugo Herbelin	2017-04-08
\| * \|	Better support for printing constructors with let-ins.	Hugo Herbelin	2017-04-07
\|/ /
* /	Intern names bound in match patterns	Tej Chajed	2017-03-23
\|/
*	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
\|\
\| *	Document changes	Matthieu Sozeau	2016-12-02
* \|	Univs: fix bug #5180	Matthieu Sozeau	2016-11-30
\| *	Fix UGraph.check_eq!	Matthieu Sozeau	2016-11-30
\|/
*	Merge remote-tracking branch 'github/pr/339' into v8.6	Maxime Dénès	2016-11-07
\|\
* \	Merge commit 'e6edb33' into v8.6	Maxime Dénès	2016-11-07
\|\ \
\| * \|	More explicit name for status of unification constraints.	Maxime Dénès	2016-11-07
\| \| *	Lets Hints/Instances take an optional pattern	Matthieu Sozeau	2016-11-03
* \| \|	Fixing error localisation bug introduced in fixing #5142 (21e1d501e17c).	Hugo Herbelin	2016-10-29
\| \|/ \|/\|
* \|	Merge remote-tracking branch 'github/pr/337' into v8.6	Maxime Dénès	2016-10-28
\|\ \
\| * \|	Complete overhaul of the Arguments vernacular.	Maxime Dénès	2016-10-27
* \| \|	Merge branch 'v8.5' into v8.6	Pierre-Marie Pédrot	2016-10-26
\|\ \ \
\| * \ \	Merge remote-tracking branch 'github/pr/333' into v8.5	Maxime Dénès	2016-10-25
\| \|\ \ \
\| * \| \| \|	Remove incorrect assertion in cbn (bug #4822).	Guillaume Melquiond	2016-10-22
\| \| \| \| *	Renamings to avoid confusion deprecating old names	Matthieu Sozeau	2016-10-22
\| \| \| \| *	Unification constraint handling (#4763, #5149)	Matthieu Sozeau	2016-10-22
\| \| * \| \|	Fix a bug in error printing of unif constraints	Matthieu Sozeau	2016-10-22
\| \|/ / /
\| \| \| *	Port fix for bugs 4763, 5149, previously 0b417c12e	Matthieu Sozeau	2016-10-22
\| \|_\|/ \|/\| \|
* \| \|	Merge remote-tracking branch 'gforge/v8.5' into v8.6	Matthieu Sozeau	2016-10-21
\|\\| \|
\| * \|	Revert "unification.ml: fix for bug #4763, unif regression"	Maxime Dénès	2016-10-21
\| * \|	A fix for #5097 (status of evars refined by "clear" in ltac: closed wrt evars).	Hugo Herbelin	2016-10-20
* \| \|	Attempt to improve error rendering in pattern-matching compilation (#5142).	Hugo Herbelin	2016-10-19
* \| \|	Merge branch 'v8.5' into v8.6	Pierre-Marie Pédrot	2016-10-18
\|\\| \|
* \| \|	Quick fix to unification regression #4955.	Hugo Herbelin	2016-10-17
\| \|/ \|/\|
\| *	Fixing to #3209 (Not_found due to an occur-check cycle).	Hugo Herbelin	2016-10-17
\| *	Fixing a missing constraint in consider_remaining_unif_constraints.	Hugo Herbelin	2016-10-17
* \|	Completing reverting generalization and cleaning of the return clause inference.	Hugo Herbelin	2016-10-13
* \|	Reverting generalization and cleaning of the return clause inference in v8.6.	Hugo Herbelin	2016-10-11
* \|	Merge branch 'v8.5' into v8.6	Pierre-Marie Pédrot	2016-10-08
\|\\|
* \|	Fix bug #5066: Anomaly: cannot find Coq.Logic.JMeq.JMeq.	Pierre-Marie Pédrot	2016-10-08
* \|	Fix bug #4464: "Anomaly: variable H' unbound. Please report.".	Pierre-Marie Pédrot	2016-10-07
\| *	evarconv.ml: Fix bug #4529, primproj unfolding	Matthieu Sozeau	2016-10-06