coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-12-03
\|\
\| *	Changing syntax "$(tactic)$" into "ltac:(tactic)", as discussed in WG.	Hugo Herbelin	2015-12-02
\| *	Test for bug #4149.	Pierre-Marie Pédrot	2015-11-30
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-11-29
\|\\|
\| *	Test-suite files for closed bugs	Matthieu Sozeau	2015-11-28
\| *	Closed bugs.	Matthieu Sozeau	2015-11-28
\| *	Univs: entirely disallow instantiation of polymorphic constants with	Matthieu Sozeau	2015-11-27
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-11-20
\|\\|
\| *	Fix bug #4429: eauto with arith: 70x performance regression in Coq 8.5.	Pierre-Marie Pédrot	2015-11-19
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-11-15
\|\\|
\| *	Fix bug #4412: [rewrite] (setoid_rewrite?) creates ill-typed terms.	Pierre-Marie Pédrot	2015-11-12
\| *	Fixed test-suite file for bug #3998.	Matthieu Sozeau	2015-11-12
\| *	Now closed.	Matthieu Sozeau	2015-11-11
\| *	Fix bug #3257, setoid_reflexivity should fail if not completing the goal.	Matthieu Sozeau	2015-11-11
\| *	Fix bug #4293: ensure let-ins do not contain algebraic universes in	Matthieu Sozeau	2015-11-11
\| *	Fixing bug #3554: Anomaly: Anonymous implicit argument.	Pierre-Marie Pédrot	2015-11-11
* \|	Revert "Fixing #1225: we now skip the canonically built binding contexts of"	Hugo Herbelin	2015-11-10
* \|	Fixing #1225: we now skip the canonically built binding contexts of	Hugo Herbelin	2015-11-10
* \|	Merge origin/v8.5 into trunk	Hugo Herbelin	2015-11-10
\|\\|
\| *	Test for bug #4404.	Pierre-Marie Pédrot	2015-11-10
* \|	Merge remote-tracking branch 'origin/v8.5' into upstream-trunk	Hugo Herbelin	2015-11-07
\|\\|
\| *	Add test-suite file for #4273.	Matthieu Sozeau	2015-11-05
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-11-05
\|\\|
\| *	Univs: missing checks in evarsolve with candidates and missing a	Matthieu Sozeau	2015-11-04
\| *	Fix bug in proofs/logic.ml type_of_global_reference_knowing_conclusion	Matthieu Sozeau	2015-11-04
\| *	Test file for #4397.	Maxime Dénès	2015-11-04
\| *	Fix bug #4151: discrepancy between exact and eexact/eassumption.	Matthieu Sozeau	2015-11-02
\| *	Refresh rigid universes as well, and in 8.4 compatibility mode,	Matthieu Sozeau	2015-11-02
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-10-30
\|\\|
\| *	Fixing another instance of bug #3267 in eauto, this time in the	Hugo Herbelin	2015-10-29
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-10-29
\|\\|
\| *	Univs: fix bug #4375, accept universe binders on (co)-fixpoints	Matthieu Sozeau	2015-10-28
\| *	Fix bugs 4389, 4390 and 4391 due to wrong handling of universe names	Matthieu Sozeau	2015-10-27
\| *	Two test-suite files for bugs 3974 and 3975	Pierre Letouzey	2015-10-26
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-10-26
\|\\|
\| *	Backtracking on interpreting toplevel calls to exact in scope determined	Hugo Herbelin	2015-10-24
\| *	Bug #3956 is fixed.	Matthieu Sozeau	2015-10-21
* \|	Removing test for bug #3956.	Pierre-Marie Pédrot	2015-10-21
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-10-19
\|\\|
\| *	Test for #4372 (anomaly in inversion in the presence of fake dependency).	Hugo Herbelin	2015-10-19
\| *	Test for bug #4325.	Pierre-Marie Pédrot	2015-10-17
* \|	Merge branch 'v8.5' into trunk	Maxime Dénès	2015-10-16
\|\\|
\| *	Test file for #4346: Set is no longer of type Type	Maxime Dénès	2015-10-15
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-10-12
\|\\|
\| *	Adding test for bug #4366.	Pierre-Marie Pédrot	2015-10-11
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-10-10
\|\\|
\| *	Refine fix for handling of the universe contexts of hints, depending on	Matthieu Sozeau	2015-10-09
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-10-09
\|\\|
\| *	Univs: fix bug #4161.	Matthieu Sozeau	2015-10-08
\| *	Fix bug #4069: f_equal regression.	Matthieu Sozeau	2015-10-07