coq - The formal proof system

Age	Commit message (Expand)	Author
2002-10-09	retour en arriere concernant la recherche d'occurence modulo expansion des le...	barras
2002-10-09	Preuve du lemme de Rolle	desmettr
2002-10-09	MAJ pour modification dans Rcomplet	desmettr
2002-10-09	Suppression d'un lemme redondant	desmettr
2002-10-09	Proof of Heine's theorem	desmettr
2002-10-09	maj	filliatr
2002-10-08	Subst ne fait pas clear sur x:=e	filliatr
2002-10-08	maj	filliatr
2002-10-07	Une fonction de moins dans .mli	coq
2002-10-07	Lazy manuelles dans le code	coq
2002-10-07	* empty log message *	desmettr
2002-10-07	* empty log message *	courant
2002-10-07	Quelques resultats complementaires	desmettr
2002-10-07	Affaiblissement des hypotheses dans TAF_gen	desmettr
2002-10-07	Make sure that bin/parser exists when checking that it works	bertot
2002-10-07	maj	filliatr
2002-10-06	correcting the treatment of many tactics that use quant_hyp in file xlate.ml	bertot
2002-10-05	Lazy experimentale temporaire...	coq
2002-10-05	pretty s'appellait prettyp mais il est revenu sous son ancien nom	herbelin
2002-10-04	Ajout du lemme derivable_pt_lim_power	desmettr
2002-10-04	Preuve de Bolzano-Weierstrass	desmettr
2002-10-04	Re-introduce the treatement of Tacticals that Hugo had already done in	bertot
2002-10-03	Intégration des modifs de la V7.3.1	herbelin
2002-10-03	Previous version did compile but did not make it possible to actually run	bertot
2002-10-03	Simplification suite MAJ 3.06	herbelin
2002-10-03	maj	filliatr
2002-10-02	Changements Omega	courant
2002-10-02	* empty log message *	desmettr
2002-10-02	Fonctions Ln et puissance	desmettr
2002-10-02	debian pkg now recommends proof general	courant
2002-10-02	Omega can now elim hyps of type False. Therefore, it knows how to deal	courant
2002-10-02	maj	filliatr
2002-10-01	Adding the congruence closure tactics (CC and CCsolve).	corbinea
2002-10-01	Oops...	coq
2002-10-01	backslahs foireux	filliatr
2002-10-01	maj	filliatr
2002-10-01	Table fonctionnelle dans autorewrite	coq
2002-10-01	Vraie substitutivite de autohints	coq
2002-10-01	Cool dev/Makefile's	coq
2002-10-01	bug de noms long pour eqT.	clrenard
2002-09-30	Comparaisons des types pendant le sous-typage reactive	coq
2002-09-30	maj	filliatr
2002-09-29	Activation du hash-consing	herbelin
2002-09-29	Hash-consing pour kernel_name	herbelin
2002-09-29	Réparation hash_consing	herbelin
2002-09-29	Complétion filtrage	herbelin
2002-09-29	Que des niveaux d'univers frais dans le type des constantes globales	herbelin
2002-09-29	Modifs diverses	herbelin
2002-09-29	Que des niveaux d'univers frais dans le type des constantes globales	herbelin
2002-09-27	Filtrage redondant	herbelin