coq - The formal proof system

Age	Commit message (Expand)	Author
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
2009-05-10	- Addition of "Hint Resolve ->" and "Hint Resolve <-" continued: it	herbelin
2009-04-25	- Fixing #2090 (occur check missing when trying to solve evar-evar equation).	herbelin
2009-04-20	Fix test output mentionning an existential number that changed.	msozeau
2009-04-20	Fix wrong pattern in Morphisms. Fix bug scripts to reflect the fact that	msozeau
2009-04-16	Fix bug #2089: correctly dealing with parameters and real arguments in	msozeau
2009-04-14	Fix and actually beautify the bug script to adapt to the new measure	msozeau
2009-04-10	Fix premature optimisation in dependent induction: even variable args need	msozeau
2009-04-08	- Backport of 12053 (fixing parsing segfault bug #2087) and 12058 (fixing	herbelin
2009-03-30	Add tests for quote	glondu
2009-03-29	Avoid inadvertent declaration of "on" as a keyword. New syntax is	msozeau
2009-03-28	Rewrite of Program Fixpoint to overcome the previous limitations:	msozeau
2009-03-26	Fixes in Program well-founded definitions:	msozeau
2009-03-19	coq_makefile: -c and -shared conflict; tacinterp: delay evaluation of tactic ...	barras
2009-03-16	Cleaning/improving the use of the "in" clause (e.g. "unfold foo in H at 4"	herbelin
2009-03-04	illegal tactic application was having Ltac interpreter loop	barras
2009-02-23	Add support for dependent "destruct" over terms in dependent types.	herbelin
2009-02-09	commited complexity test for exponential behavior of unification	barras
2009-02-06	Fixing #2044 (bad printing of primitive notation at the head of	herbelin
2009-02-06	From v8.2 to trunk:	herbelin
2009-02-04	Report r11631 from 8.2 and handle non-dependent goals better in	msozeau
2009-01-22	Fixes in the documentation of [dependent induction] and test-suite	msozeau
2009-01-20	Fixing bug #1918 (no occur-check in Meta unification was done yet!).	herbelin
2009-01-20	- Fixing bug 1891 (abusive instantiations of evar arguments in	herbelin
2009-01-19	The initial state evar numbering increased. Fix output message in a test.	puech
2009-01-18	Backporting from v8.2 to trunk:	herbelin
2009-01-13	- Standardized prefix use of "Local"/"Global" modifiers as decided in	herbelin
2009-01-12	Fix a bunch of bugs related to setoid_rewrite, unification and evars:	msozeau
2009-01-11	- Deactivation of dynamic loading on Mac OS 10.5 (see bug #2024).	herbelin
2009-01-07	Uniformisation of some error messages + added test on setoid rewrite.	herbelin
2009-01-04	Fixed bugs #2001 (search_guard was overwriting the guard index given	herbelin