coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
...
\| *	Fix bug #4103: forgot to allow unfolding projections of cofixpoints like	Matthieu Sozeau	2015-03-03
\| *	Fix bug #4101, noccur_evar's expand_projection can legitimately fail	Matthieu Sozeau	2015-03-03
\| *	Fix bug #4097.	Matthieu Sozeau	2015-03-02
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-02-28
\|\\|
\| *	Adding a test for bug #3612.	Pierre-Marie Pédrot	2015-02-27
\| *	Test for bug #3249.	Pierre-Marie Pédrot	2015-02-27
\| *	Fix test for #3467, I had moved it in a dumb way.	Maxime Dénès	2015-02-27
\| *	Add support so that the type of a match in an inductive type with let-in	Hugo Herbelin	2015-02-27
\| *	Fixing first part of bug #3210 (inference of pattern-matching return	Hugo Herbelin	2015-02-27
\| *	Fix test for #3848, still open.	Maxime Dénès	2015-02-27
\| *	Moving test for #3467 to closed after PMP's fix.	Maxime Dénès	2015-02-27
\| *	Fix test-suite files for bugs #2456 and #3593, still open.	Maxime Dénès	2015-02-27
\| *	Add test-suite file for #3649.	Maxime Dénès	2015-02-27
\| *	Moving tests for #2456 and #3593 to "opened" until they're fixed.	Maxime Dénès	2015-02-27
\| *	Made test for #3392 rely less on unification.	Maxime Dénès	2015-02-27
\| *	Moving test of #3848 to "opened".	Maxime Dénès	2015-02-27
\| *	Test for #2602, which seems now fixed.	Maxime Dénès	2015-02-26
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-02-26
\|\\|
\| *	Test for bug #3298.	Pierre-Marie Pédrot	2015-02-26
\| *	Revert "Fixing bug #4035 (support for dependent destruction within ltac code)."	Maxime Dénès	2015-02-26
\| *	Moving test for bug #3681 as closed.	Pierre-Marie Pédrot	2015-02-26
\| *	Univs: Fix Check calling the kernel to retype in the wrong environment.	Matthieu Sozeau	2015-02-24
* \|	Merge branch 'v8.5' into trunk	Enrico Tassi	2015-02-23
\|\\|
\| *	Fix some typos in comments.	Guillaume Melquiond	2015-02-23
\| *	Test for #3953 (subst in evar instances).	Hugo Herbelin	2015-02-23
\| *	Fixing test #2830.	Pierre-Marie Pédrot	2015-02-23
\| *	Fixing test for bug #3071.	Pierre-Marie Pédrot	2015-02-23
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-02-23
\|\\|
\| *	Moving test for bug #3071.	Pierre-Marie Pédrot	2015-02-21
\| *	Test for bug #4078.	Pierre-Marie Pédrot	2015-02-21
* \|	Removed tests for #3900 and #3944 as open bugs.	Hugo Herbelin	2015-02-21
\| *	A fix for #3993 (not fully applied term to destruct when eqn is given).	Hugo Herbelin	2015-02-20
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-02-18
\|\\|
\| *	Fix bug #3938	Matthieu Sozeau	2015-02-18
\| *	Remove some dead code and add test-suite file.	Matthieu Sozeau	2015-02-16
\| *	Add test-suite file for #3960.	Matthieu Sozeau	2015-02-16
\| *	Test for bug #3922.	Pierre-Marie Pédrot	2015-02-16
\| *	Fixing bug #4035 (support for dependent destruction within ltac code).	Hugo Herbelin	2015-02-16
\| *	Test for #2946 (trunk bug with let's in unification).	Hugo Herbelin	2015-02-16
\| *	Fixing test for bug #3944.	Pierre-Marie Pédrot	2015-02-16
\| *	Test for bug #3944.	Pierre-Marie Pédrot	2015-02-16
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-02-15
\|\\|
\| *	Fix test-suite file. Check that definitions do work when sharing is	Matthieu Sozeau	2015-02-15
\| *	Test for bug #3490.	Pierre-Marie Pédrot	2015-02-15
\| *	Test for bug #3916.	Pierre-Marie Pédrot	2015-02-15
\| *	Fixing test-suite.	Pierre-Marie Pédrot	2015-02-15
\| *	Test for bug #4016.	Pierre-Marie Pédrot	2015-02-14
\| *	Univs: fix bug #3755. We were missing refreshements of universes in	Matthieu Sozeau	2015-02-14
\| *	Univs: When computing the level of an inductive including indices, lets	Matthieu Sozeau	2015-02-14
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-02-13
\|\\|