coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Ajout map_rawconstr	herbelin	2002-10-13
*	Mise en place d'ensembles de notations symboliques pour nat, Z et R	herbelin	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-13
*	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-12
*	maj	filliatr	2002-10-11
*	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-10
*	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-09
*	Subst ne fait pas clear sur x:=e	filliatr	2002-10-08
*	maj	filliatr	2002-10-08
*	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-07
*	correcting the treatment of many tactics that use quant_hyp in file xlate.ml	bertot	2002-10-06
*	Lazy experimentale temporaire...	coq	2002-10-05
*	pretty s'appellait prettyp mais il est revenu sous son ancien nom	herbelin	2002-10-05
*	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-04
*	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-03
*	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-02
*	Adding the congruence closure tactics (CC and CCsolve).	corbinea	2002-10-01
*	Oops...	coq	2002-10-01