coq - The formal proof system

Age	Commit message (Expand)	Author
2016-03-25	Test suite file for a bug in int31 arithmetic fixed a while ago.	Maxime Dénès
2016-01-21	Merge branch 'v8.5'	Pierre-Marie Pédrot
2016-01-20	Update copyright headers.	Maxime Dénès
2015-10-02	Merge branch 'v8.5'	Pierre-Marie Pédrot
2015-10-02	Fix test-suite file	Matthieu Sozeau
2015-06-24	Extend test-suite for the positivity checker.	Arnaud Spiwack
2015-01-12	Update headers.	Maxime Dénès
2014-07-22	Add test-suite file for guard condition on cofixpoints.	Maxime Dénès
2014-04-09	Add another critical bug to the test-suite.	Maxime Dénès
2014-01-15	Test case containing a proof of false due to a DeBruijn off-by-one error in the	Maxime Dénès
2013-12-21	Test case for the buggy commutative cut subterm rule.	Maxime Dénès
2013-12-17	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-09-20	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-19	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-01-18	Unset Asymmetric Patterns	pboutill
2012-08-08	Updating headers.	herbelin
2012-07-05	Kills the useless tactic annotations "in \|- *"	letouzey
2011-10-05	Fixing critical inductive polymorphism bug found by Bruno.	herbelin
2011-04-08	Applying and reworking Tom Prince's patch for test-suite/failure/universes2.v	herbelin
2010-09-23	Fix inconsistency in Prop/Set conversion check	glondu
2010-07-24	Updated all headers for 8.3 and trunk	herbelin
2010-05-20	Added examples for checking that the guard condition excludes subterms	herbelin
2010-03-24	Fixed bug #2260 (check of resolution of all evars in the declaration	herbelin
2009-10-25	Improved the treatment of Local/Global options (noneffective Local on	herbelin
2009-10-08	Fixed a bug introduced in revision 12265.	herbelin
2009-09-17	Delete trailing whitespaces in all .{v,ml} files	glondu
2009-08-11	Relatively ad hoc fix to an ill-typed instantiation bug in type	herbelin
2008-12-02	fixed kernel bug (de Bruijn) + test-suite	barras
2008-11-27	added tests for hyps reordering	barras
2008-08-04	Évolutions diverses et variées.	herbelin
2008-07-25	Correction d'une incohérence de typage des inductifs polymorphes: les	herbelin
2008-04-22	fixed universes bug related to module inclusion	barras
2008-04-21	test module include w.r.t. universe constraints	barras
2007-10-16	Vérification que "rewrite in" se comporte comme "rewrite" et échoue	herbelin
2007-09-06	Itération sur les sous-termes dans la vérification de la condition de garde	herbelin
2007-02-21	Fixed the pseudo-cicularity problem due to the with operator on Module Type.	soubiran
2007-01-19	Tests de référence circulaire au sous-typage de module (pour mémoire)	herbelin
2007-01-17	Correction bug #1302	herbelin
2006-12-13	test condition de garde	barras
2006-10-27	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-13	Adaptation des tests suite à la modification de Rewrite .. in (r9201)	notin
2006-08-22	+ Changing "in <hyp>" to "in <clause>" (no at, no InValue and no	jforest
2006-06-23	Stricte positivité en présence de types inductifs imbriqués avec paramètr...	herbelin
2006-06-22	Deux vérifications que le polymorphisme de sorte des inductifs ne fonctionne...	herbelin