coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Fixed some printing bugs.	herbelin	2010-04-18
*	Moved Case3.v from ideal features to success (it works since 8.2).	herbelin	2010-04-17
*	Remove only *.v.log files in clean of test-suite/Makefile	glondu	2010-04-13
*	Recovering 8.2 behavior of "simple (e)apply" (and hence of "(e)auto").	herbelin	2010-04-11
*	Prettier test-suite/Makefile	glondu	2010-04-10
*	Optimized need for delimiters when disjoint scopes for strings and	herbelin	2010-04-10
*	Use the Makefile in test-suite/check	glondu	2010-04-10
*	Makefile for the test-suite	glondu	2010-04-10
*	Fix typos in test-suite script	glondu	2010-04-10
*	Test for bug #2231 (unexpected error when using let/if over an inductive	herbelin	2010-04-10
*	Commit 12906 continued (forgotten file).	herbelin	2010-04-07
*	Granting wish #2251 thanks to commit 12900 solved bug 1416.v (which	herbelin	2010-04-07
*	New model for user-driven translation of tokens in coqdoc	herbelin	2010-04-06
*	Granting wish #2251 (forbidding rewriting a term reduced to an evar)	herbelin	2010-04-05
*	Tests for bug report #2244 (pattern-unification with abstraction over Meta's)	herbelin	2010-04-05
*	Small things about coqdoc + fixing lettuple.v test (part of bug #2289)	herbelin	2010-03-30
*	Several bug-fixes and improvements of coqdoc	herbelin	2010-03-29
*	Fixing bug #2279 (printing nested let-in was in exponential time)	herbelin	2010-03-27
*	Applied greenrd's patch to fix bug 2255 (injection failed to	herbelin	2010-03-27
*	Fixed bug #2260 (check of resolution of all evars in the declaration	herbelin	2010-03-24
*	Added automatic expansion on the left of recursive notations	herbelin	2010-03-23
*	Fix bug in backtracking.	vgross	2010-03-23
*	fixed minor pbs with test cases	barras	2010-03-12
*	fixed confusion between number of cstr arguments and number of pattern variab...	barras	2010-03-12
*	introduced lazy computation of size info in the guard condition	barras	2010-03-11
*	Minimal test suite for search commands	puech	2010-03-11
*	New backtracking code + fix bug #2082.	vgross	2010-02-26
*	Fix NumbersSyntax.out	letouzey	2010-02-13
*	ajout test de fied_simplify_eq in	barras	2010-02-10
*	bugs/.../1784.v: revert Matthieu's recent fix, since Program has been made co...	letouzey	2010-02-10
*	minor change in test-suite/output/NumberSyntax.out: a BigN.t_ instead of BigN.t	letouzey	2010-01-29
*	New version of 12650 that was broken (supporting again records when	herbelin	2010-01-12
*	revert commit 12650 for the moment, since it breaks MSetAVL	letouzey	2010-01-12
*	Temporary fix to compensate the loss of descent on dependent	herbelin	2010-01-12
*	Errors issued by reduction tactics (e.g. pattern) were not caught by "try".	herbelin	2010-01-04
*	Regression test for bug #2145 (Groebner failing with "not eq" hypotheses).	herbelin	2009-12-30
*	Fixing bug #2193: computation of dependencies in the "match" return	herbelin	2009-12-30
*	Fixing bug #2146 (broken selection of occurrences in "change").	herbelin	2009-12-30
*	Renouncing to have the option "Automatic Introduction" on by default.	herbelin	2009-12-29
*	Improving descend_in_conjunctions (using a combinators instead of a tactic)	herbelin	2009-12-29
*	In "simpl c" and "change c with d", c can be a pattern.	herbelin	2009-12-24
*	Made the side-conditions of lemmas always come last when chaining "apply in"	herbelin	2009-12-13
*	Revision 12557 continued (better rendering of dependent rewrite)	herbelin	2009-12-13
*	Still continuing r12485-12486, r12549, r12556 (cleaning around name generation)	herbelin	2009-12-03
*	Continuing r12485-12486 and r12549 (cleaning around name generation)	herbelin	2009-12-02
*	Remove interface plugin	glondu	2009-12-02
*	Continuing r12485-12486 (cleaning around name generation)	herbelin	2009-12-01
*	Fix backtracking heuristic in typeclass resolution.	msozeau	2009-11-30
*	Added support for definition of fixpoints using tactics.	herbelin	2009-11-27
*	Substitute terms for evars-as-goals as soon as they are solved in	msozeau	2009-11-27