coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Fixing bug #3093 by adding the asked test case.	ppedrot	2013-07-25
*	Bugfix: Fixing #3050	ppedrot	2013-06-27
*	Protection against "Bad recursive type" in w_unify0 (bug #3036).	herbelin	2013-05-08
*	Added a unit test for bug #2230.	ppedrot	2013-04-27
*	Finer fix for bug 3017, mark unresolvability only of goals that are	msozeau	2013-04-18
*	Like in r16346, do not filter local definitions (here in the	herbelin	2013-04-17
*	Added regression test for bug #3023 which was solved by Matthieu's	herbelin	2013-04-16
*	Equality: avoid some unprotected List.nth (fix #2837)	letouzey	2013-04-10
*	Enrich test-suite with a test for #3022.	ppedrot	2013-04-08
*	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-25
*	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-21
*	Check a list length before doing a List.chop (fix #3000)	letouzey	2013-03-20
*	Fix for bug #3004 (thanks Hugo!)	letouzey	2013-03-18
*	A slightly more efficient test of well-typedness of restriction of	herbelin	2013-02-21
*	Fixed bug #2981 (anomaly NotASort in Retyping due to collision between	herbelin	2013-02-05
*	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-29
*	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-28
*	Unset Asymmetric Patterns	pboutill	2013-01-18
*	Fixed bug #2930: folded let-in's were hiding a violation to the occur	herbelin	2012-11-25
*	Fixing #2836 (materialize_evar might refine as a side effect the	herbelin	2012-07-29
*	Continuing r15459: it helps testing occur-check early in some	herbelin	2012-07-06
*	ZArith + other : favor the use of modern names instead of compat notations	letouzey	2012-07-05
*	Fixing bug #2817 (occur check was not done up to instantiation of	herbelin	2012-06-20
*	Implicit arguments of Definition are taken from the type when given by the user.	pboutill	2012-04-27
*	Bug 2733 : { } implicits and Fixpoints	pboutill	2012-04-17
*	Fixing tauto "special" behavior on singleton types w/ 2 parameters (bug #2680).	herbelin	2012-04-15
*	Repair two tests	letouzey	2012-04-12
*	Generalized the use of evar candidates in type inference unification:	herbelin	2012-03-20
*	Fix bugs related to Program integration.	msozeau	2012-03-19
*	Fixing bug #2732 (anomaly when using the tolerance for writing	herbelin	2012-03-18
*	Fixing vm_compute bug #2729 (function used to decompose constructors	herbelin	2012-03-13
*	Backtracking on r14876 (fix for bug #2267): extra scopes might be	herbelin	2012-01-05
*	Fixing Arguments Scope bug when too many scopes are given (bug #2667).	herbelin	2012-01-04
*	Extend the computation of dependencies in pattern-matching compilation	herbelin	2011-11-21
*	Fixing bug #2640 and variants of it (inconsistency between when and	herbelin	2011-11-17
*	Fixing bug #1834 (de Bruijn indices bug in pattern-matching compilation).	herbelin	2011-11-16
*	Regression tests for bugs #2613 and #2616.	herbelin	2011-10-25
*	New strategy to infer return predicate of match construct when	herbelin	2011-10-25
*	Mod_subst: Attempt to fix #2608	letouzey	2011-10-24
*	Fix bug #2473 due to wrong folding of the evar environment	msozeau	2011-10-18
*	Fix inductive coercion code in Program (bug #2378)	msozeau	2011-10-18
*	Fix bug #2586 and enhance clsubst* as well as a side effect	msozeau	2011-10-18
*	Fix bug #2456 and wrong unfolding of lets in the goal due to [unfold] doing z...	msozeau	2011-10-17
*	test-suite: non-regression test for bug #2603	letouzey	2011-10-12