coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	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
* \|	Simplification and improvement of "subst x" in such a way that it	Hugo Herbelin	2014-05-08
* \|	Fixing test-suite for bug #3043.	Pierre-Marie Pédrot	2014-05-08
* \|	Fixing output test-suite: since universe polymorphism, the Print command	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
*	Comment in Funind.v test-suite file	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
*	- Fix arity handling in retyping (de Bruijn bug!)	Matthieu Sozeau	2014-05-06
*	Fix restrict_universe_context removing some universes that do appear in the t...	Matthieu Sozeau	2014-05-06
*	Fix declarations of monomorphic assumptions	Matthieu Sozeau	2014-05-06
*	- Fix RecTutorial, and mutual induction schemes getting the wrong names.	Matthieu Sozeau	2014-05-06
*	- Fixes for canonical structure resolution (check that the initial term indee...	Matthieu Sozeau	2014-05-06
*	This commit adds full universe polymorphism and fast projections to Coq.	Matthieu Sozeau	2014-05-06
*	Update test-suite Makefile to handle coq-prog-args	Jason Gross	2014-05-02
*	Fixing #3293 (eta-expansion at "match" printing time was failing	Hugo Herbelin	2014-04-28
*	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
*	Add another critical bug to the test-suite.	Maxime Dénès	2014-04-09
*	Adapt test-suite to -I is ML only	Pierre Boutillier	2014-04-09
*	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
*	Remove option -g as it is non-portable yet does not have any effect on the te...	Guillaume Melquiond	2014-04-04
*	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
*	test for apply + TC resolution	Enrico Tassi	2014-03-26
*	nanoPG: better copy/paste	Enrico Tassi	2014-03-13
*	Never suppress the typing constraint of bound variables whose name was	Pierre-Marie Pédrot	2014-03-01
*	Pos.compare_cont takes the comparison as first argument	Pierre Boutillier	2014-02-28