coq - The formal proof system

Age	Commit message (Expand)	Author
2001-09-14	MAJ vis à vis de la nouvelle non-localité des Remark/Fact	herbelin
2001-09-12	* empty log message *	mohring
2001-09-10	changement du make depend en vu du make reals	letouzey
2001-09-10	bug de rename_global modulaire corrige'	letouzey
2001-09-09	Nettoyage reduce_to_ind et one_step_reduce	herbelin
2001-08-10	Prsing	herbelin
2001-08-10	Parsing	herbelin
2001-08-07	Passage au nouveau Destruct	herbelin
2001-08-05	Expérimentation de NewDestruct et parfois NewInduction	herbelin
2001-07-21	Remplacement du tableau du nombre d'args utiles pour la réduction des Cases ...	herbelin
2001-07-18	Ajout de la contrib sur les graphes	mohring
2001-07-10	Setoid_rewrite -> Rewrite	clrenard
2001-07-10	Ajout des fichiers pour le Ring pour setoides	clrenard
2001-07-10	Changement de place de la tactique Setoid_rewrite	clrenard
2001-07-10	Ajout d'un Ring pour setoides	clrenard
2001-07-05	correction bug Omega	filliatr
2001-07-02	Evar et Zeta ne sont plus implicites dans Delta (mais le restent dans Compute...	herbelin
2001-07-02	Nettoyage/restructuration des ensembles d'indicateurs de réductions	herbelin
2001-06-27	Reduction du terme preuve fourni par Field	delahaye
2001-06-27	correction d'un bug de Correctness (pour Y Bertot)	filliatr
2001-06-27	Reduction tres significative du terme preuve	delahaye
2001-06-26	Les tacticques Setoid_replace/rewrite peuvent maintenant reecrire sous une	clrenard
2001-06-25	Découpage de g_tactic.ml4 en 2 (pour satisfaire les contraintes de la compil...	herbelin
2001-06-25	liste des equiv exportee	clrenard
2001-06-22	2 bugs: typevarlist pour inductifs + args pour flexibles	letouzey
2001-06-20	Ajout d'un Setoid_rewrite et meilleure resolution des petits sous-buts géné...	clrenard
2001-06-19	Un bug corrige.	clrenard
2001-06-12	Ajout de la tactique Setoid_replace.	clrenard
2001-05-29	Facilites pour le debogguage des univers.	coq
2001-05-28	Pretty -> Prettyp	filliatr
2001-05-28	patch Claudio	filliatr
2001-05-28	nettoyage	filliatr
2001-05-25	Oups: flingait les Dglob dans optimize	letouzey
2001-05-23	amelioration des messages d'erreurs vis a vis des evars	barras
2001-05-22	maj	letouzey
2001-05-22	suite du musée des horreurs	letouzey
2001-05-22	ordre des inductifs + axiome-type	letouzey
2001-05-18	Modification afin de permettre plusieurs modifs successives d'une commande	clrenard
2001-05-14	mise en place extraction haskell	filliatr
2001-05-14	réparation Ring (simplifications)	filliatr
2001-05-11	application patch Claudio	filliatr
2001-05-11	bug cast	letouzey
2001-05-10	exemples Magic	letouzey
2001-05-10	message 'is defined' seulement en mode verbose	filliatr
2001-05-10	retouche de extract_inductive_declaration	letouzey
2001-05-09	nettoyage extraction	filliatr
2001-05-09	cleanup + comments, toujours	letouzey
2001-05-07	integration de field a fourier	mayero
2001-05-04	commentaires	letouzey
2001-05-03	Changement de la structure des points fixes	barras