coq - The formal proof system

Age	Commit message (Expand)	Author
2012-07-05	ZArith + other : favor the use of modern names instead of compat notations	letouzey
2012-03-23	Fix the test-suite by removing any Reset in the scripts	letouzey
2012-03-20	Fixing alpha-conversion bug #2723 introduced in r12485-12486.	herbelin
2011-12-17	Added ability to take the type of applied metas into account when	herbelin
2011-04-28	Fixing an "apply -> ... in hyp" bug (the hyp was considered as a fixed	herbelin
2011-03-13	Fix inductive_template building ill-typed evars, and update test-suite scripts	msozeau
2010-04-11	Recovering 8.2 behavior of "simple (e)apply" (and hence of "(e)auto").	herbelin
2010-01-12	New version of 12650 that was broken (supporting again records when	herbelin
2010-01-12	revert commit 12650 for the moment, since it breaks MSetAVL	letouzey
2010-01-12	Temporary fix to compensate the loss of descent on dependent	herbelin
2009-12-29	Improving descend_in_conjunctions (using a combinators instead of a tactic)	herbelin
2009-12-13	Made the side-conditions of lemmas always come last when chaining "apply in"	herbelin
2009-10-25	Restore (and test) broken chaining of lemmas in "apply in" in presence	herbelin
2009-10-25	Add support for remaining side-conditions in "apply in as".	herbelin
2009-09-17	Delete trailing whitespaces in all .{v,ml} files	glondu
2009-07-08	Reactivation of pattern unification of evars in apply unification, in	herbelin
2008-12-09	About "apply in":	herbelin
2008-10-26	Backtrack sur commit 11467 (tentative d'optimisation meta_instance qui	herbelin
2008-10-19	Retour en arrière pour raison de compatibilité sur la suppression du nf_evar	herbelin
2008-10-18	- Merge modifs coq_makefile.ml4 de la 8.1 vers le trunk (commit 11429)	herbelin
2008-06-18	Propagation des révisions 11144 et 11136 de la 8.2 vers le trunk	herbelin
2008-04-28	Petites corrections vis à vis des commits 10860, 10859, 10850	herbelin
2008-04-27	Quelques bricoles autour de l'unification:	herbelin
2008-04-23	Prise en compte des coercions dans les clauses "with" même si le type	herbelin
2008-04-03	Chgts mineurs:	herbelin
2008-04-01	Ajout des propriétés $Id:$ là où elles n'existaient pas ou n'étaient	herbelin
2007-05-28	Contrôle de la compatibilité de apply via une information dans les	herbelin
2007-05-24	Unification suite: petits affinements pour préserver la compatibilité	herbelin
2007-05-22	Nouvelle stratégie d'unification des types des with-bindings dans	herbelin
2006-12-13	Alignement de la politique de renommage de rename_bound_var (utilisé pour	herbelin
2006-11-13	Correction typo	herbelin
2006-11-10	Ajout de dépliage de l'énoncé, si besoin est, dans apply in	herbelin
2006-10-24	Test apply in	herbelin