coq - The formal proof system

Age	Commit message (Expand)	Author
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
2009-11-12	Restore test-suite/csdp.cache erased from svn by mistake	letouzey
2009-11-12	BigQ / BigN / BigZ syntax and scope improvements (sequel to 12504)	letouzey
2009-11-12	Repair interpretation of numeral for BigQ, add a printer (close #2160)	letouzey
2009-11-11	Redoing broken commit r12498 (fixing bug #2167 + attempt to test the	herbelin
2009-11-11	Fixing bug #2167 + attempt to test the compatibility of a more robust	herbelin
2009-11-11	Test for bug #2168, forgotten in r12496.	herbelin
2009-11-11	Fixed bug #2168 (closing a section may have as side-effect the erasure	herbelin
2009-11-11	Improving abbreviations/notations + backtrack of semantic change in r12439	herbelin
2009-11-09	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12483 85f007b7-540e-0...	fbesson
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-08	Fixed a bug introduced in revision 12265.	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-24	Micromega doc : psatz Z -> psatz Z 2	fbesson
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-18	micromega: better handling of exponentiation + correction of test-suite termi...	fbesson
2009-09-17	Delete trailing whitespaces in all .{v,ml} files	glondu
2009-08-25	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12294 85f007b7-540e-0...	fbesson
2009-08-15	+ csdp.cache	fbesson
2009-08-13	Death of "survive_module" and "survive_section" (the first one was	herbelin
2009-08-11	Ensures that let-in's in arities of inductive types work well. Maybe not	herbelin
2009-08-11	Relatively ad hoc fix to an ill-typed instantiation bug in type	herbelin
2009-07-30	psatz Z -> psatz Z 1	fbesson
2009-07-24	Remove the barely-used/obsolete/undocumented syntax "conditional <tac> rewrite"	letouzey
2009-07-20	Move some examples for groebner into a test-suite file	letouzey
2009-07-15	- Granted wish #2138 (support for local binders in syntax of Record fields).	herbelin
2009-07-08	Reactivation of pattern unification of evars in apply unification, in	herbelin
2009-06-06	Fixing bug #2106 ("match" compilation with multi-dependent constructor).	herbelin
2009-06-02	Adding a regression test about Bauer's example on coq-club of	herbelin
2009-06-02	Fix script file using the "Manual Implicit" flag.	msozeau
2009-05-11	micromega: proof compression bugfix	fbesson