coq - The formal proof system

Age	Commit message (Expand)	Author
2010-04-13	Remove only *.v.log files in clean of test-suite/Makefile	glondu
2010-04-11	Recovering 8.2 behavior of "simple (e)apply" (and hence of "(e)auto").	herbelin
2010-04-10	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-07	Commit 12906 continued (forgotten file).	herbelin
2010-04-07	Granting wish #2251 thanks to commit 12900 solved bug 1416.v (which	herbelin
2010-04-06	New model for user-driven translation of tokens in coqdoc	herbelin
2010-04-05	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-03-30	Small things about coqdoc + fixing lettuple.v test (part of bug #2289)	herbelin
2010-03-29	Several bug-fixes and improvements of coqdoc	herbelin
2010-03-27	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-24	Fixed bug #2260 (check of resolution of all evars in the declaration	herbelin
2010-03-23	Added automatic expansion on the left of recursive notations	herbelin
2010-03-23	Fix bug in backtracking.	vgross
2010-03-12	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-11	introduced lazy computation of size info in the guard condition	barras
2010-03-11	Minimal test suite for search commands	puech
2010-02-26	New backtracking code + fix bug #2082.	vgross
2010-02-13	Fix NumbersSyntax.out	letouzey
2010-02-10	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-01-29	minor change in test-suite/output/NumberSyntax.out: a BigN.t_ instead of BigN.t	letouzey
2010-01-12	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-04	Errors issued by reduction tactics (e.g. pattern) were not caught by "try".	herbelin
2009-12-30	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-29	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-24	In "simpl c" and "change c with d", c can be a pattern.	herbelin
2009-12-13	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-03	Still continuing r12485-12486, r12549, r12556 (cleaning around name generation)	herbelin
2009-12-02	Continuing r12485-12486 and r12549 (cleaning around name generation)	herbelin
2009-12-02	Remove interface plugin	glondu
2009-12-01	Continuing r12485-12486 (cleaning around name generation)	herbelin
2009-11-30	Fix backtracking heuristic in typeclass resolution.	msozeau
2009-11-27	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-26	Fixing xml theory file export (was not consistent with coqdoc file	herbelin
2009-11-13	Fix test-suite scripts: [Generalizable Variables] and small	msozeau