coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	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
*	11511 continued (bug in set.out + incohérence dans "Theorem with"	herbelin	2008-10-28
*	- Fixed many "Theorem with" bugs.	herbelin	2008-10-27
*	Backtrack sur commit 11467 (tentative d'optimisation meta_instance qui	herbelin	2008-10-26
*	Generalized implementation of generalization.	msozeau	2008-10-23
*	Affichage des notations récursives:	herbelin	2008-10-22
*	Retour en arrière pour raison de compatibilité sur la suppression du nf_evar	herbelin	2008-10-19
*	- Merge modifs coq_makefile.ml4 de la 8.1 vers le trunk (commit 11429)	herbelin	2008-10-18
*	test-suite: more utf8 tests, a test of ! ? and so on in rewrites	letouzey	2008-10-14
*	Minor fixes related to coqdoc and --interpolate and the dependent	msozeau	2008-10-03