coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-12-03
\|\
\| *	Adding a target report to test-suite's Makefile to get a short summary.	Hugo Herbelin	2015-12-02
\| *	Improving syntax of pat/constr introduction pattern so that	Hugo Herbelin	2015-12-02
\| *	Changing syntax "$(tactic)$" into "ltac:(tactic)", as discussed in WG.	Hugo Herbelin	2015-12-02
* \|	New algorithm for universe cycle detections.	Jacques-Henri Jourdan	2015-12-01
\| *	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
\| *	Fixing the "parsing rules with idents later declared as keywords" problem.	Hugo Herbelin	2015-11-26
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-11-26
\|\\|
\| *	Fixing a vm_compute bug in the presence of let-ins among the	Hugo Herbelin	2015-11-22
\| *	Fixing a bug of adjust_subst_to_rel_context.	Hugo Herbelin	2015-11-22
\| *	Fixing kernel bug in typing match with let-ins in the arity.	Hugo Herbelin	2015-11-22
* \|	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
\| *	Fixing logical bugs in the presence of let-ins in computiong primitive	Hugo Herbelin	2015-11-18
* \|	Fixing output test Cases.v.	Pierre-Marie Pédrot	2015-11-15
* \|	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
* \|	Updating test-suite after Bracketing Last Introduction Pattern set by	Hugo Herbelin	2015-11-10
* \|	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
* \|	Adapting output test inference.v after c23f0cab6 (experimenting	Hugo Herbelin	2015-11-08
\| *	Fixing output test Existentials.v after eec77191b.	Hugo Herbelin	2015-11-07
\| *	Tests for syntax "Show id" and [id]:tac (shelved or not).	Hugo Herbelin	2015-11-07
* \|	Merge remote-tracking branch 'origin/v8.5' into upstream-trunk	Hugo Herbelin	2015-11-07
\|\\|
\| *	Fixing complexity file f_equal.v.	Hugo Herbelin	2015-11-06
\| *	Fixing complexity issue with f_equal. Thanks to J.-H. Jourdan	Hugo Herbelin	2015-11-06
\| *	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
\| *	Hint Cut documentation and cleanup of printing (was duplicated and	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
\|\\|
\| *	Handle side-effects of Vernacular commands inside proofs better, so that	Matthieu Sozeau	2015-10-29
\| *	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
\|\\|
\| *	Fix test suite after Matthieu's ed7af646f2e486b.	Maxime Dénès	2015-10-28