coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Move some examples for groebner into a test-suite file	letouzey	2009-07-20
*	- Granted wish #2138 (support for local binders in syntax of Record fields).	herbelin	2009-07-15
*	Reactivation of pattern unification of evars in apply unification, in	herbelin	2009-07-08
*	Fixing bug #2106 ("match" compilation with multi-dependent constructor).	herbelin	2009-06-06
*	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-06-02
*	micromega: proof compression bugfix	fbesson	2009-05-11
*	- Addition of "Hint Resolve ->" and "Hint Resolve <-" continued: it	herbelin	2009-05-10
*	- Fixing #2090 (occur check missing when trying to solve evar-evar equation).	herbelin	2009-04-25
*	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-20
*	Fix bug #2089: correctly dealing with parameters and real arguments in	msozeau	2009-04-16
*	Fix and actually beautify the bug script to adapt to the new measure	msozeau	2009-04-14
*	Fix premature optimisation in dependent induction: even variable args need	msozeau	2009-04-10
*	- Backport of 12053 (fixing parsing segfault bug #2087) and 12058 (fixing	herbelin	2009-04-08
*	Add tests for quote	glondu	2009-03-30
*	Avoid inadvertent declaration of "on" as a keyword. New syntax is	msozeau	2009-03-29
*	Rewrite of Program Fixpoint to overcome the previous limitations:	msozeau	2009-03-28
*	Fixes in Program well-founded definitions:	msozeau	2009-03-26
*	coq_makefile: -c and -shared conflict; tacinterp: delay evaluation of tactic ...	barras	2009-03-19
*	Cleaning/improving the use of the "in" clause (e.g. "unfold foo in H at 4"	herbelin	2009-03-16
*	illegal tactic application was having Ltac interpreter loop	barras	2009-03-04
*	Add support for dependent "destruct" over terms in dependent types.	herbelin	2009-02-23
*	commited complexity test for exponential behavior of unification	barras	2009-02-09
*	Fixing #2044 (bad printing of primitive notation at the head of	herbelin	2009-02-06
*	From v8.2 to trunk:	herbelin	2009-02-06
*	Report r11631 from 8.2 and handle non-dependent goals better in	msozeau	2009-02-04
*	Fixes in the documentation of [dependent induction] and test-suite	msozeau	2009-01-22
*	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-20
*	The initial state evar numbering increased. Fix output message in a test.	puech	2009-01-19
*	Backporting from v8.2 to trunk:	herbelin	2009-01-18
*	- Standardized prefix use of "Local"/"Global" modifiers as decided in	herbelin	2009-01-13
*	Fix a bunch of bugs related to setoid_rewrite, unification and evars:	msozeau	2009-01-12
*	- Deactivation of dynamic loading on Mac OS 10.5 (see bug #2024).	herbelin	2009-01-11
*	Uniformisation of some error messages + added test on setoid rewrite.	herbelin	2009-01-07
*	Fixed bugs #2001 (search_guard was overwriting the guard index given	herbelin	2009-01-04
*	Regression test for bug #1967	herbelin	2009-01-02
*	Conséquence renommage canonique de refl_equal en eq_refl.	herbelin	2009-01-02
*	- Fixed bug #2021 (uncaught exception with injection/discriminate when	herbelin	2009-01-01
*	- Optimized "auto decomp" which had a (presumably) exponential in	herbelin	2008-12-26
*	Nettoyage des variables Coq et amélioration de coqmktop. Les	notin	2008-12-19
*	Finish fix for the treatment of [inverse] in [setoid_rewrite], making a	msozeau	2008-12-16
*	Fix for syntax changes in test-suite scripts.	msozeau	2008-12-16
*	About "apply in":	herbelin	2008-12-09
*	improved simpl	barras	2008-12-03
*	Add new directory for pre-compilation of files needed for further tests.	herbelin	2008-12-02
*	Miscellaneous fixes and improvements:	herbelin	2008-12-02
*	fixed kernel bug (de Bruijn) + test-suite	barras	2008-12-02
*	Test case for previous commit.	msozeau	2008-11-27