coq - The formal proof system

Age	Commit message (Expand)	Author
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
2009-01-02	Regression test for bug #1967	herbelin
2009-01-02	Conséquence renommage canonique de refl_equal en eq_refl.	herbelin
2009-01-01	- Fixed bug #2021 (uncaught exception with injection/discriminate when	herbelin
2008-12-26	- Optimized "auto decomp" which had a (presumably) exponential in	herbelin
2008-12-19	Nettoyage des variables Coq et amélioration de coqmktop. Les	notin
2008-12-16	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-09	About "apply in":	herbelin
2008-12-03	improved simpl	barras
2008-12-02	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-11-27	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-26	closed bug 1898: fold x in x; added a reordering primitive tactic	barras
2008-11-23	Fixed bug #2006 (type constraint on Record was not taken into account) +	herbelin
2008-11-14	Add missing test-suite files for closed bugs.	msozeau
2008-11-13	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11583 85f007b7-540e-0...	barras
2008-11-09	- 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-07	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-04	Adaptation to ocaml 3.11 new semantics of String.index_from (see bug #1974)	herbelin
2008-11-02	test-suite/ideal-features/{apply.v -> eapply_evar.v}	glondu
2008-10-28	11511 continued (bug in set.out + incohérence dans "Theorem with"	herbelin
2008-10-27	- Fixed many "Theorem with" bugs.	herbelin
2008-10-26	Backtrack sur commit 11467 (tentative d'optimisation meta_instance qui	herbelin