coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
...
\| *	camlp4: grep away warnings in output/* tests	Enrico Tassi	2015-03-30
\| *	Adding test for bug #4165.	Pierre-Marie Pédrot	2015-03-29
\| *	Fully fixing bug #3491 (anomaly when building _rect scheme in the	Hugo Herbelin	2015-03-25
\| *	Another example about the consequence of a wrong computation of the	Hugo Herbelin	2015-03-25
\| *	Updating test-suite (see previous commit).	Hugo Herbelin	2015-03-24
\| *	Fixing computation of non-recursively uniform arguments in the	Hugo Herbelin	2015-03-24
\| *	Fixing wrong rel_context in checking positivity condition.	Hugo Herbelin	2015-03-24
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-03-23
\|\\|
\| *	Qed export -> Qed exporting	Enrico Tassi	2015-03-22
* \|	Merge branch 'v8.5' into trunk	Arnaud Spiwack	2015-03-13
\|\\|
\| *	Add some tests for tryif	Jason Gross	2015-03-13
\| *	Fix regression in HoTT_coq_014.v	Enrico Tassi	2015-03-11
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-03-11
\|\\|
\| *	admit: replaced by give_up + Admitted (no proof_admitted : False, close #4032)	Enrico Tassi	2015-03-11
\| *	Do not display the status of monomorphic constants unless in universe-polymor...	Guillaume Melquiond	2015-03-09
\| *	Test for bug #2951.	Pierre-Marie Pédrot	2015-03-08
\| *	Test for #4035 (dependent destruction from Ltac).	Hugo Herbelin	2015-03-07
* \|	Merge branch 'v8.5' into trunk	Pierre Letouzey	2015-03-06
\|\\|
\| *	Fix testsuite with respect to the new formatting of Fail messages.	Guillaume Melquiond	2015-03-05
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-03-04
\|\\|
\| *	Fix test-suite file, this is open.	Matthieu Sozeau	2015-03-03
\| *	Fix bug #3732: firstorder was using detyping to build existential	Matthieu Sozeau	2015-03-03
\| *	Add missing test-suite files and update gitignore.	Matthieu Sozeau	2015-03-03
\| *	Add a test-suite file ensuring coinductives with primitive projections	Matthieu Sozeau	2015-03-03
\| *	Fix test-suite file, this is currently a wontfix, but keep the	Matthieu Sozeau	2015-03-03
\| *	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
\| *	Fixing complexity tests for #4076.	Maxime Dénès	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
\| *	Another test for a variant of complexity problem #4076 (thanks to A. Mortberg).	Hugo Herbelin	2015-02-25
* \|	Other tests for decl mode, coming from reference manual.	Hugo Herbelin	2015-02-24
\| *	Univs: Fix Check calling the kernel to retype in the wrong environment.	Matthieu Sozeau	2015-02-24