coq - The formal proof system

Age	Commit message (Expand)	Author
2003-11-24	Prise en compte des defs syntaxiques dans is_global et global_reference qui p...	herbelin
2003-10-10	Affichage des buts par Pfedit pour utilisation par les tactiques (Setoid_repl...	herbelin
2003-10-07	Correction du bug 335 et Export/Require Export dans un module	coq
2003-09-12	Indépendance vis à vis de Declare	herbelin
2003-03-31	Ajout d'un message à FailTac	herbelin
2003-03-31	factorisation des "constant" dans les contrib/* ( maintenant dans coqlib )	corbinea
2003-03-29	eq fusionne avec eqT et devient par défaut sur Type,	herbelin
2003-03-12	* empty log message *	barras
2003-01-22	Correction bug réecriture à la racine pour le sétoide Prop.	clrenard
2002-12-09	Ajout Simpl et Change sur des sous-termes	herbelin
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-23	Ajout de la syntaxe "Theorem f [binders] : t", comme pour Definition et Local	herbelin
2002-10-01	bug de noms long pour eqT.	clrenard
2002-09-29	Que des niveaux d'univers frais dans le type des constantes globales	herbelin
2002-08-02	Modules dans COQ\!\!\!\!	coq
2002-05-29	Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et co...	herbelin
2002-05-14	Changement de eq en eqT comme equivalence de setoide par defaut.	clrenard
2002-05-02	Minor correction of get_lem_name	coq
2002-03-04	Nouveau Rewrite-in plus economique	barras
2001-12-13	compat ocaml 3.03	filliatr
2001-11-20	Fusion de declare/add_constant, declare/add_parameter et add_discharged_constant	herbelin
2001-11-05	GROS COMMIT:	barras
2001-10-11	Suppression option immediate_discharge; nettoyage de Declare et conséquences	herbelin
2001-10-09	Suppression des arguments sur les constantes, inductifs et constructeurs	barras
2001-09-20	Transparent	barras
2001-09-19	Deplacement des setoides.	clrenard
2001-09-18	Modification de l'emplacement des fichiers pour les setoides.	clrenard
2001-08-10	Parsing	herbelin
2001-07-10	Ajout du .ml pour la tactique Setoid_replace	clrenard