coq - The formal proof system

Age	Commit message (Expand)	Author
2007-07-13	New bootstrapping, improved, Makefile system	corbinea
2007-05-20	- Propagation des evars non résolues vers les with_bindings; permet par exemple	herbelin
2007-05-15	corrections bug dans l'implem de int31	bgregoir
2007-04-05	On n'a plus besoin de compiler les anciens fichiers de functionnal induction ...	jforest
2006-09-20	Declarative Proof Language: main commit	corbinea
2006-03-22	Made pretyping a functor over a coercion implementation. Pretyping.Default us...	msozeau
2006-03-22	- Réintroduction d'un parseur de pattern (q_constr.ml4) à usage de	herbelin
2006-03-13	Update of Subtac contrib. Add {wf n R} as an alternative to {struct n}.	msozeau
2006-02-08	Julien:	bertot
2006-02-01	New version of functional induction / inversion. By Julien Forest,	coq
2005-12-30	maj	coq
2005-12-26	Renommage des Ppnew en Pp (et déplacement dans parsing); renommage des G_*...	herbelin
2005-12-26	Suppression des parseurs et printeurs v7; suppression du traducteur (mcanisme...	herbelin
2005-11-18	maj	coq
2005-11-07	Modifications in the .depend files for the contrib/recdef directory	bertot
2005-08-17	new congruence	corbinea
2005-07-15	Subtac: traitement correct des existentielles et de la rÃ©cursion.	coq
2005-07-15	reflexive tauto	corbinea
2005-05-25	Added subtac contrib.	coq
2005-05-20	New command: "Print Ltac qualid" to print user defined tactics.	sacerdot
2005-03-16	tactiques prouveurs premier ordre dans contrib/dp/	coq
2005-02-04	Ajout g_xml.ml4 et cic2Xml.ml	herbelin
2004-08-26	maj	filliatr
2004-07-29	maj	filliatr
2004-07-16	MAJ	herbelin
2004-05-04	maj	filliatr
2004-01-28	maj	filliatr
2004-01-15	maj	filliatr
2003-10-16	Ground update + Linear removal	corbinea
2003-07-02	suppression de newtauto	corbinea
2003-06-15	Ground major update ... mmm, sounds exciting !	corbinea
2003-05-26	moved engine.ml4 to ground.ml4, added option 'Ground Depth'	corbinea
2003-04-25	Added the Ground tactic.	corbinea
2003-03-12	* Ajout du traducteur nouvelle syntaxe *	barras
2003-02-28	maj	filliatr
2003-02-27	The contribution of Pierre Courtieu on generating specialized induction schemes	bertot
2003-02-24	Bringing Linear back to life (Still somewhat buggy).	corbinea
2003-01-23	Ajout de LinearIntuition; Ajout de New(Tauto\|Intuition\|LinearIntuition).	corbinea
2002-11-14	Réforme de l'interprétation des termes :	herbelin
2002-11-05	Intégration des modifs de la branche mowgli :	herbelin
2002-10-01	Adding the congruence closure tactics (CC and CCsolve).	corbinea
2002-09-20	maj	filliatr
2002-09-20	maj	filliatr
2002-08-02	Modules dans COQ\!\!\!\!	coq
2002-06-07	extraction vers scheme	letouzey
2002-05-29	Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et co...	herbelin
2001-12-19	contrib/interface/dad.ml4 had no real need of streams, it should have been	bertot
2001-12-19	reparation du make depend et du .depend	letouzey
2001-06-25	Les réduction dans les hypothèses s'appliquent maintenant au corps de la d�...	herbelin
2001-06-25	Découpage de g_tactic.ml4 en 2 (pour satisfaire les contraintes de la compil...	herbelin