coq - The formal proof system

Age	Commit message (Expand)	Author
2009-03-20	Directory 'contrib' renamed into 'plugins', to end confusion with archive of ...	letouzey
2008-03-06	Plug the new setoid implemtation in, leaving the original one commented	msozeau
2006-11-13	Encore des _sym au lieu de _comm	herbelin
2005-02-02	The statement of the compatibility theorem for addition and multiplication	sacerdot
2004-10-01	The "Add Setoid" command now has a new argument "as name" that is used	sacerdot
2004-09-03	Ported to the new implementation of setoid_*.	sacerdot
2004-07-16	Nouvelle en-tête	herbelin
2003-11-29	Remplacement des fichiers .v ancienne syntaxe de theories, contrib et states ...	herbelin
2003-11-13	moins unaire au niveau 35, tactiques simple_induction et simple_destruct, Loc...	barras
2003-11-01	Finalement, niveau 0 pour l'argument du '-' uniare, pour eviter que les entie...	herbelin
2003-10-30	Parsing du moins unaire au niveau de l'application qui n'a pas besoin d'etre ...	herbelin
2003-10-22	reorganisation des niveaux (ex: = est a 70)	barras
2003-09-21	Changement de la politique de V8only: V8only tout seul signifie	herbelin
2003-05-21	Mise en conformite de la precedence du '-' unaire avec celle de Notations (su...	herbelin
2003-05-21	Mise en conformite de la precedence du '-' unaire avec celle de Notations	herbelin
2003-03-12	* empty log message *	barras
2002-12-02	Remplacement Grammar par Notation	herbelin
2002-12-02	Remplacement de Syntactic Definition par Notation	herbelin
2002-04-17	Uniformisation (Qed/Save et Implicits Arguments)	herbelin
2001-09-18	Modification de l'emplacement des fichiers pour les setoides.	clrenard
2001-08-07	Passage au nouveau Destruct	herbelin
2001-08-05	Expérimentation de NewDestruct et parfois NewInduction	herbelin
2001-07-10	Ajout des fichiers pour le Ring pour setoides	clrenard