coq - The formal proof system

Age	Commit message (Expand)	Author
2010-06-13	Fixed bug #2314 (inversion using not checking the correctness of its arguments	herbelin
2010-06-11	Mainly made that evarconv is able to solve "?n = (fun x => x) ?n" (sic).	herbelin
2010-06-09	Automatic introduction of names given before ":" in Lemma's and	herbelin
2010-06-09	Backported r13080 (support for open terms in ltac matching) from trunk to v8.3.	herbelin
2010-06-06	Added support for Ltac-matching terms with variables bound in the pattern	herbelin
2010-06-04	Grobner.v removed	pottier
2010-06-03	plugin groebner updated and renamed as nsatz; first version of the doc of nsa...	pottier
2010-04-29	Remove the svn-specific $Id$ annotations	letouzey
2010-04-17	Moved Case3.v from ideal features to success (it works since 8.2).	herbelin
2010-04-11	Recovering 8.2 behavior of "simple (e)apply" (and hence of "(e)auto").	herbelin
2010-04-07	Commit 12906 continued (forgotten file).	herbelin
2010-03-23	Added automatic expansion on the left of recursive notations	herbelin
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-02-10	ajout test de fied_simplify_eq in	barras
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	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-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-13	Fix test-suite scripts: [Generalizable Variables] and small	msozeau
2009-11-11	Test for bug #2168, forgotten in r12496.	herbelin
2009-11-11	Improving abbreviations/notations + backtrack of semantic change in r12439	herbelin
2009-11-08	Restructuration of command.ml + generic infrastructure for inductive schemes	herbelin
2009-10-30	Attempt to capture on time unification errors for "with" bindings.	herbelin
2009-10-29	Revision 12439 continued, printing part (notations to names behave	herbelin
2009-10-28	Integrate a few improvements on typeclasses and Program from the equations br...	msozeau
2009-10-28	Made that notations to names behave like the names they refer to wrt	herbelin
2009-10-26	Local/Global revision 12418 continued	herbelin
2009-10-26	Adapted test unfold.v after eq gets its argument maximally inserted	herbelin
2009-10-25	Restore (and test) broken chaining of lemmas in "apply in" in presence	herbelin
2009-10-25	Add support for remaining side-conditions in "apply in as".	herbelin
2009-10-25	Improved the treatment of Local/Global options (noneffective Local on	herbelin
2009-10-17	Fixed a notation bug when extending binder_constr with empty levels	herbelin
2009-10-04	Removal of trailing spaces.	serpyc
2009-09-27	Fixed a bug in the interaction between dEqThen and inject_at_positions	herbelin
2009-09-27	Fixed two tests that was incorrectly typed in former revisions 12348 and 12356.	herbelin
2009-09-27	Delay the choice of eliminator in destruct/induction until we know if	herbelin
2009-09-22	Add the option to automatically introduce variables declared before the	msozeau
2009-09-20	Only one "in" clause in "destruct" even for a multiple "destruct".	herbelin
2009-09-17	Delete trailing whitespaces in all .{v,ml} files	glondu
2009-08-11	Ensures that let-in's in arities of inductive types work well. Maybe not	herbelin