coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Ensuring all .v files end with a newline to make "sed -i" work better on them.	Hugo Herbelin	2017-08-21
*	Bump year in headers.	Pierre-Marie Pédrot	2017-07-04
*	BigNums: remove files about BigN,BigZ,BigQ (now in an separate git repo)	Pierre Letouzey	2017-06-13
*	Update various comments to use "template polymorphism"	Gaetan Gilbert	2017-04-11
*	Test suite file for a bug in int31 arithmetic fixed a while ago.	Maxime Dénès	2016-03-25
*	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-01-21
\|\
\| *	Update copyright headers.	Maxime Dénès	2016-01-20
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-10-02
\|\\|
\| *	Fix test-suite file	Matthieu Sozeau	2015-10-02
* \|	Extend test-suite for the positivity checker.	Arnaud Spiwack	2015-06-24
\|/
*	Update headers.	Maxime Dénès	2015-01-12
*	Add test-suite file for guard condition on cofixpoints.	Maxime Dénès	2014-07-22
*	Add another critical bug to the test-suite.	Maxime Dénès	2014-04-09
*	Test case containing a proof of false due to a DeBruijn off-by-one error in the	Maxime Dénès	2014-01-15
*	Test case for the buggy commutative cut subterm rule.	Maxime Dénès	2013-12-21
*	test guard condition against feature incompatible with prop-ext	Bruno Barras	2013-12-17
*	Tentative fix of the guardedness checker by Christine and me. All stdlib and ...	Matthieu Sozeau	2013-12-17
*	Fix name clash in "failure/inductive.v".	xclerc	2013-09-20
*	Merge "circular_subtyping?.v" tests into a single "circular_subtyping.v" test.	xclerc	2013-09-20
*	Merge "inductive?.v" tests into a single "inductive.v" test.	xclerc	2013-09-20
*	Use "Fail" rather than rely on exit code.	xclerc	2013-09-20
*	Uminus.v : prepare this test file for the use of Fail	letouzey	2013-09-19
*	universes-buraliforti-redef.v : repair a match after Pierre B. syntax changes	letouzey	2013-09-19
*	Unset Asymmetric Patterns	pboutill	2013-01-18
*	Updating headers.	herbelin	2012-08-08
*	Kills the useless tactic annotations "in \|- *"	letouzey	2012-07-05
*	Fixing critical inductive polymorphism bug found by Bruno.	herbelin	2011-10-05
*	Applying and reworking Tom Prince's patch for test-suite/failure/universes2.v	herbelin	2011-04-08
*	Fix inconsistency in Prop/Set conversion check	glondu	2010-09-23
*	Updated all headers for 8.3 and trunk	herbelin	2010-07-24
*	Added examples for checking that the guard condition excludes subterms	herbelin	2010-05-20
*	Fixed bug #2260 (check of resolution of all evars in the declaration	herbelin	2010-03-24
*	Improved the treatment of Local/Global options (noneffective Local on	herbelin	2009-10-25
*	Fixed a bug introduced in revision 12265.	herbelin	2009-10-08
*	Delete trailing whitespaces in all .{v,ml} files	glondu	2009-09-17
*	Relatively ad hoc fix to an ill-typed instantiation bug in type	herbelin	2009-08-11
*	fixed kernel bug (de Bruijn) + test-suite	barras	2008-12-02
*	added tests for hyps reordering	barras	2008-11-27
*	Évolutions diverses et variées.	herbelin	2008-08-04
*	Correction d'une incohérence de typage des inductifs polymorphes: les	herbelin	2008-07-25
*	fixed universes bug related to module inclusion	barras	2008-04-22
*	test module include w.r.t. universe constraints	barras	2008-04-21
*	Vérification que "rewrite in" se comporte comme "rewrite" et échoue	herbelin	2007-10-16
*	Itération sur les sous-termes dans la vérification de la condition de garde	herbelin	2007-09-06
*	Fixed the pseudo-cicularity problem due to the with operator on Module Type.	soubiran	2007-02-21
*	Tests de référence circulaire au sous-typage de module (pour mémoire)	herbelin	2007-01-19
*	Correction bug #1302	herbelin	2007-01-17
*	test condition de garde	barras	2006-12-13
*	Check that sort-polymorphic inductive types is not too lax	herbelin	2006-10-27
*	Cette dérivation de paradoxe passait en V8.1beta	herbelin	2006-10-27