coq - The formal proof system

Age	Commit message (Expand)	Author
2019-02-04	Primitive integers	Maxime Dénès
2018-10-04	test-suite: cleaning	Vincent Laporte
2018-10-04	test-suite: rename a few files	Vincent Laporte
2018-03-30	Change Implicit Arguments to Arguments in test-suite	Jasper Hugunin
2018-03-09	Merge PR #407: Fix SR breakage due to allowing fixpoints on non-rec values	Maxime Dénès
2018-03-08	Fix SR breakage due to allowing fixpoints on non-rec values	Matthieu Sozeau
2018-02-27	Update headers following #6543.	Théo Zimmermann
2017-08-21	Ensuring all .v files end with a newline to make "sed -i" work better on them.	Hugo Herbelin
2017-07-04	Bump year in headers.	Pierre-Marie Pédrot
2017-06-13	BigNums: remove files about BigN,BigZ,BigQ (now in an separate git repo)	Pierre Letouzey
2017-04-11	Update various comments to use "template polymorphism"	Gaetan Gilbert
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