coq - The formal proof system

Age	Commit message (Expand)	Author
2014-01-25	Adding a test for bug #3023.	Pierre-Marie Pédrot
2014-01-10	Fix bug#2080: error message on Ltac name clash with primitive tactics	xclerc
2013-12-16	Added test-suite for bug #2990.	Pierre-Marie Pédrot
2013-12-12	Better unification for [projT1] and [proj1_sig].	Jason Gross
2013-12-06	Fix the refine related test-suite files to account for the new refine.	Arnaud Spiwack
2013-12-02	Test case for bug#2848.	xclerc
2013-09-20	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	Update test for bug 2846 in order to use "Fail".	xclerc
2013-09-20	Use "Fail" rather than rely on exit code.	xclerc
2013-08-04	Added test for bug #2846.	ppedrot
2013-08-04	Added a test for bug #3062.	ppedrot
2013-08-01	Added a test for bug #3088.	ppedrot
2013-07-29	Tentative fix for #3054: we refresh universes in a term generated	ppedrot
2013-07-25	Fixing bug #3093 by adding the asked test case.	ppedrot
2013-06-27	Bugfix: Fixing #3050	ppedrot
2013-05-08	Protection against "Bad recursive type" in w_unify0 (bug #3036).	herbelin
2013-04-27	Added a unit test for bug #2230.	ppedrot
2013-04-18	Finer fix for bug 3017, mark unresolvability only of goals that are	msozeau
2013-04-17	Like in r16346, do not filter local definitions (here in the	herbelin
2013-04-16	Added regression test for bug #3023 which was solved by Matthieu's	herbelin
2013-04-10	Equality: avoid some unprotected List.nth (fix #2837)	letouzey
2013-04-08	Enrich test-suite with a test for #3022.	ppedrot
2013-03-25	Enrich test-suite with a test for #2928	letouzey
2013-03-25	Enrich test-suite with a test for #2734	letouzey
2013-03-25	Add the test-case of bug 2750 in the test-suite	letouzey
2013-03-21	Robust display of NotConvertibleTypeField errors (fix #3008, #2995)	letouzey
2013-03-21	Firstorder: record with defined field aren't conjonctions (fix #2629)	letouzey
2013-03-21	Printmod: fresh fake namespaces for non-visible modules (fix #2668, #2983)	letouzey
2013-03-20	Check a list length before doing a List.chop (fix #3000)	letouzey
2013-03-18	Fix for bug #3004 (thanks Hugo!)	letouzey
2013-02-21	A slightly more efficient test of well-typedness of restriction of	herbelin
2013-02-05	Fixed bug #2981 (anomaly NotASort in Retyping due to collision between	herbelin
2013-01-29	Added a file for testing regression of bug #2955 (anomaly in simpl in	herbelin
2013-01-29	Fixing bug #2969 (admit failing after Grab Existential Variables due	herbelin
2013-01-28	Fixed bug #2966 (de Bruijn error in computation of heads for coercions).	herbelin
2013-01-28	Fixing one part of #2830 (anomaly "defined twice" due to nested calls to	herbelin
2013-01-18	Unset Asymmetric Patterns	pboutill
2012-11-25	Fixed bug #2930: folded let-in's were hiding a violation to the occur	herbelin
2012-07-29	Fixing #2836 (materialize_evar might refine as a side effect the	herbelin
2012-07-06	Continuing r15459: it helps testing occur-check early in some	herbelin
2012-07-05	ZArith + other : favor the use of modern names instead of compat notations	letouzey
2012-06-20	Fixing bug #2817 (occur check was not done up to instantiation of	herbelin
2012-04-27	Implicit arguments of Definition are taken from the type when given by the user.	pboutill
2012-04-17	Bug 2733 : { } implicits and Fixpoints	pboutill
2012-04-15	Fixing tauto "special" behavior on singleton types w/ 2 parameters (bug #2680).	herbelin
2012-04-12	Repair two tests	letouzey
2012-03-20	Generalized the use of evar candidates in type inference unification:	herbelin
2012-03-19	Fix bugs related to Program integration.	msozeau