coq - The formal proof system

Age	Commit message (Expand)	Author
2002-10-13	Nettoyage	herbelin
2002-10-13	Déplacement de + et * aux niveaux de précédence 7 et 6	herbelin
2002-10-13	Déplacement de + et * aux niveaux de précédence 7 et 6	herbelin
2002-10-13	Première proposition d'un type ML exprimant la syntaxe de constr; nettoyage	herbelin
2002-10-13	Mise en place de 'Scope' pour gérer des ensembles de notations - phase 1; ha...	herbelin
2002-10-12	réparation de la protection contre les clauses indiscernables de TACTIC EXTE...	herbelin
2002-10-12	Notation 2:Check et 2:Eval	herbelin
2002-10-12	Restriction sur la forme des Syntactic Definition et re-localisation en fonct...	herbelin
2002-10-12	Nettoyage	herbelin
2002-10-12	Forcer la réouverture d'un fichier explicitement requis même si le	herbelin
2002-10-11	maj	filliatr
2002-10-10	Ajout ClassicalFacts	herbelin
2002-10-10	gestion coherente de l'option -R et des Require A.B.C.	barras
2002-10-10	Nametab permet de definir le meme truc la deuxieme fois	coq
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