coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	- 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
*	fixed bug 1791: simpl was performing eta expansion	barras	2008-11-27
*	added tests for hyps reordering	barras	2008-11-27
*	closed bug 1898: fold x in x; added a reordering primitive tactic	barras	2008-11-26
*	Fixed bug #2006 (type constraint on Record was not taken into account) +	herbelin	2008-11-23
*	Add missing test-suite files for closed bugs.	msozeau	2008-11-14
*	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11583 85f007b7-540e-0...	barras	2008-11-13
*	- Correction erreur dans test output Notation.v	herbelin	2008-11-09
*	Add test-suite file related to discussion of syntax of implicit binders.	msozeau	2008-11-09
*	Slight change of the semantics of user-given casts: they don't really	msozeau	2008-11-07
*	- Ajout possibilité de lancer ocamldebug sur coqide	herbelin	2008-11-07
*	Add some example uses of the new record features in Record.v:	msozeau	2008-11-07
*	Fix a bug in the specialization by unification tactic related to the problems	msozeau	2008-11-07
*	Adaptation to ocaml 3.11 new semantics of String.index_from (see bug #1974)	herbelin	2008-11-04
*	test-suite/ideal-features/{apply.v -> eapply_evar.v}	glondu	2008-11-02