coq - The formal proof system

Age	Commit message (Expand)	Author
2006-09-19	added congruence improvement	corbinea
2006-04-28	Suppression des fichiers .cvsignore, rendus obsolètes par le systèmes des '...	notin
2006-01-21	Messages de idtac et fail peuvent maintenant être des listes de string, int ...	herbelin
2005-12-26	Suppression des parseurs et printeurs v7; suppression du traducteur (mcanisme...	herbelin
2005-12-02	Changement des named_context	gregoire
2005-11-02	Types inductifs parametriques	mohring
2005-08-17	new congruence	corbinea
2005-02-18	Standardisation of function names about global references (especially, renami...	herbelin
2005-02-12	Uniformisation de destApplication en destApp	herbelin
2005-02-06	Nettoyage et documentation de Library	herbelin
2005-01-14	Inductive.{type_of_inductive,type_of_constructor,arities_of_specif} changed	sacerdot
2004-07-16	Nouvelle en-tête	herbelin
2004-03-15	oops	corbinea
2004-03-14	minor changes	corbinea
2004-03-14	congruence now handles disequalities	corbinea
2004-02-06	correction de bugs de congruence et firstorder (inductifs)	corbinea
2004-01-09	bugs avec Pose et Assert	barras
2003-12-09	cc update	corbinea
2003-12-02	error messages adjustement	corbinea
2003-11-29	Remplacement des fichiers .v ancienne syntaxe de theories, contrib et states ...	herbelin
2003-11-29	ground->firstorder, cc-> congruence, CC final commit	corbinea
2003-11-26	just forgot something in previous commit	corbinea
2003-11-26	removal of CC.v lemata in cc (deprecated)	corbinea
2003-11-25	CC: added injection theory	corbinea
2003-11-20	Code simplification in CC	corbinea
2003-10-03	Cacher les .v8	herbelin
2003-05-25	Ground and CCsolve updates	corbinea
2003-03-31	factorisation des "constant" dans les contrib/* ( maintenant dans coqlib )	corbinea
2002-11-14	Réforme de l'interprétation des termes :	herbelin
2002-10-01	Adding the congruence closure tactics (CC and CCsolve).	corbinea