coq - The formal proof system

Age	Commit message (Expand)	Author
2020-11-20	Granting #9816: apply in takes several hypotheses.	Hugo Herbelin
2018-09-14	Fixing yet a source of dependency on alphabetic order in unification.	Hugo Herbelin
2018-03-30	Change Implicit Arguments to Arguments in test-suite	Jasper Hugunin
2016-02-13	Do not give a name to anonymous evars anymore. See bug #4547.	Pierre-Marie Pédrot
2015-09-08	Ensuring that patterns of the form pat/constr move the hypotheses replacing	Hugo Herbelin
2015-08-02	Fixing test apply.v (had wrong option name).	Hugo Herbelin
2015-08-02	Reverting 16 last commits, committed mistakenly using the wrong push command.	Hugo Herbelin
2015-08-02	Fixing test apply.v (had wrong option name).	Hugo Herbelin
2015-08-02	Granting Jason's request for an ad hoc compatibility option on	Hugo Herbelin
2015-02-23	Fixing occur-check which was too strong in unification.ml.	Hugo Herbelin
2014-09-29	Restoring non-uniform delta on local and global constants in 2nd order	Hugo Herbelin
2014-09-10	Example for apply and evars.	Hugo Herbelin
2014-09-03	Yes another remaining clearing bug with 'apply in'.	Hugo Herbelin
2014-09-02	Another fix than 19a7a5789c to avoid descend_in_conjunction to use	Hugo Herbelin
2014-09-02	An apply test.	Hugo Herbelin
2014-08-29	Not using a "cut" in descend_in_conjunctions induced more success. We	Hugo Herbelin
2014-08-25	"allows to", like "allowing to", is improper	Jason Gross
2014-08-25	Fixing a bug introduced in the extension of 'apply in' + simplifying code.	Hugo Herbelin
2014-08-18	A reorganization of the "assert" tactics (hopefully uniform naming	Hugo Herbelin
2014-08-16	Fixing too restrictive detection of resolution of evars in "apply in"	Hugo Herbelin
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