coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Move closed bug 3314	Jason Gross	2014-06-10
*	Add a test-case for bug #3314 proving False	Jason Gross	2014-06-10
*	Mark some progress in the HoTT/coq test-suite	Jason Gross	2014-06-08
*	ind_tables: always declare side effects (Closes: HOTT#110)	Enrico Tassi	2014-06-08
*	A bug has been closed (HoTT/coq #105)	Jason Gross	2014-06-03
*	Adding test-suite for bug #3355.	Pierre-Marie Pédrot	2014-05-30
*	Fix unification of non-unfoldable primitive projections in evarconv.	Matthieu Sozeau	2014-05-16
*	Test-suite for bug #3259.	Pierre-Marie Pédrot	2014-05-13
*	Update various polyproj bugs w.r.t. latest trunk	Jason Gross	2014-05-12
*	Add appropriate Fail(s) to opened bugs	Jason Gross	2014-05-10
*	Move opened bugs to bugs/opened	Jason Gross	2014-05-10
*	Add more regression tests for univ poly/prim proj	Jason Gross	2014-05-10
*	Refresh universes for Ltac's type_of, as the term can be used anywhere,	Matthieu Sozeau	2014-05-09
*	Merge branch 'working-polyproj-tests' of https://github.com/JasonGross/coq in...	Matthieu Sozeau	2014-05-09
\|\
* \|	Fix second-order matching to properly check that the predicate found by	Matthieu Sozeau	2014-05-09
* \|	Fixing test-suite for bug #3043.	Pierre-Marie Pédrot	2014-05-08
* \|	Adding test-suite for bug #3242.	Pierre-Marie Pédrot	2014-05-06
\| *	Add regression tests for univ. poly. and prim proj	Jason Gross	2014-05-06
\|/
*	Keep track of universes on coercion applications even if they're not polymorp...	Matthieu Sozeau	2014-05-06
*	Refresh some universes in cases.ml as they might appear in the term.	Matthieu Sozeau	2014-05-06
*	Fix set_leq_sort refusing max(u,Set) <= Set when u is flexible.	Matthieu Sozeau	2014-05-06
*	Retype application of fix_proto to get the right universes in Program	Matthieu Sozeau	2014-05-06
*	Add regression tests for 3188 and 3265	Jason Gross	2014-04-22
*	Adding a test for bug #2923.	Pierre-Marie Pédrot	2014-04-20
*	Adding a test for bug #3285.	Pierre-Marie Pédrot	2014-04-20
*	better description of bug 3251	Enrico Tassi	2014-04-10
*	coqtop -batch refuses Back 1 but accepts Undo.	Pierre Boutillier	2014-04-10
*	By resolution of the CoqWG, instantiate must not be used now that refine works	Pierre Boutillier	2014-04-10
*	No more Coersion in Init.	Pierre Boutillier	2014-04-10
*	Define [projT3] and [proj3_sig]	Jason Gross	2014-04-10
*	Test case for bug 3037	Jason Gross	2014-04-10
*	Test case for 3164	Jason Gross	2014-04-10
*	Test case for bug 3262	Jason Gross	2014-04-10
*	Test case for bug #3217	Jason Gross	2014-04-10
*	Add a regression test for bug 3001	Jason Gross	2014-04-10
*	Test for bug #3142, actually duplicate of #3262.	Hugo Herbelin	2014-04-05
*	Fixing bug #3228 (fixing precedence of ltac variables over variables in env).	Hugo Herbelin	2014-04-05
*	Add a test case for bug 3251	Jason Gross	2014-04-02
*	Fixing bug #2900 (evar/evar unif was supposed to be treated in	Hugo Herbelin	2014-04-01
*	Adding a test for bug #3023.	Pierre-Marie Pédrot	2014-01-25
*	Fix bug#2080: error message on Ltac name clash with primitive tactics	xclerc	2014-01-10
*	Missing Fail in r16792	Pierre Boutillier	2013-12-19
*	Added test-suite for bug #2990.	Pierre-Marie Pédrot	2013-12-16
*	Better unification for [projT1] and [proj1_sig].	Jason Gross	2013-12-12
*	Fix the refine related test-suite files to account for the new refine.	Arnaud Spiwack	2013-12-06
*	Test case for bug#2848.	xclerc	2013-12-02
*	Testsuite: flatten the 'bugs/opened' directory.	xclerc	2013-11-29
*	Get rid of "shouldsucceed" subdirectory by moving tests to parent directory.	xclerc	2013-09-20
*	Get rid of "shouldfail" subdirectory by moving tests to parent directory.	xclerc	2013-09-20
*	Wrong bug identifier.	xclerc	2013-09-20