coq - The formal proof system

Age	Commit message (Expand)	Author
2001-10-22	chambardement important des fichiers auxiliaires. Nouvelle syntaxe pour les o...	letouzey
2001-10-17	Abstraction de l'immplementation de dirpath et implementation dans l'autre se...	herbelin
2001-10-12	Déplacement de global_reference dans Names pour pouvoir lier Nametab à gra...	herbelin
2001-10-12	reparation	filliatr
2001-10-09	Suppression des arguments sur les constantes, inductifs et constructeurs	barras
2001-10-01	correction de deux petits bugs: case_identité trop fort et Anomaly dans le t...	letouzey
2001-09-21	Correction due au changement de semantique de Match	delahaye
2001-09-20	Transparent	barras
2001-09-20	correction du eta_expanse	letouzey
2001-09-20	Report des modifs de Claudio	herbelin
2001-09-20	bug affichage des termes ml fournis	letouzey
2001-09-20	utilisation du nouveau get_sort_family_of	letouzey
2001-09-20	changements mineurs du test	letouzey
2001-09-20	Romega	mohring
2001-09-19	ajout du fichier CHANGES	letouzey
2001-09-19	adaptation a la nouvelle syntaxe Extract Inlined Constant	letouzey
2001-09-19	Changements de Extraction truc et Recursive Extraction	letouzey
2001-09-19	Deux nouvelles optimisations pour Cases	letouzey
2001-09-19	MAJ V7.1	herbelin
2001-09-19	Verification supplementaire avant optimisation singleton	letouzey
2001-09-19	reparation Zne	mohring
2001-09-18	travail sur le Extract Constant	letouzey
2001-09-18	Modification de l'emplacement des fichiers pour les setoides.	clrenard
2001-09-18	Romega/names/Makefile	mohring
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