coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Quelques ameliorations dans Reg	desmettr	2002-07-22
*	Nvll preuves R_dist_tri et tech_limit	mayero	2002-07-19
*	correction bugs Tauto	courant	2002-07-19
*	Regularites de pow et des sommes finies / MAJ Reg	desmettr	2002-07-19
*	Resultats de regularite de Rabsolu / MAJ de Reg	desmettr	2002-07-19
*	Quelques ameliorations...	desmettr	2002-07-19
*	* empty log message *	desmettr	2002-07-18
*	Correction d'un bug dans IsCont_pt	desmettr	2002-07-18
*	MAJ pour Sqrt_reg	desmettr	2002-07-18
*	Preuves de la continuite/derivabilite de sqrt sur R+/R+*	desmettr	2002-07-18
*	* empty log message *	desmettr	2002-07-18
*	reparation temporaire(?) a coup de MLdummy'	letouzey	2002-07-17
*	tactique Subst	filliatr	2002-07-17
*	Nettoyage de code pour la règle [id:(?1-> ?2)-> ?3\|- ?]	corbinea	2002-07-17
*	ajout de make otags utilisant otags plutot que etags	letouzey	2002-07-17
*	modification de make tags pour	letouzey	2002-07-17
*	maj	letouzey	2002-07-16
*	Pour ocamlweb	letouzey	2002-07-16
*	Souci avec example fbidon...	letouzey	2002-07-16
*	petit bug lors du passage d'hugo	letouzey	2002-07-16
*	Gros Remaniement Extraction:	letouzey	2002-07-16
*	un cas inutile dans un pattern matching	letouzey	2002-07-16
*	* empty log message *	desmettr	2002-07-16
*	* empty log message *	desmettr	2002-07-16
*	Bug dans la globalisation des arguments de tactiques primitives	herbelin	2002-07-16
*	MAJ Makefile pour Reals	desmettr	2002-07-16
*	MAJ Rtrigo pour sqrt	desmettr	2002-07-16
*	* empty log message *	desmettr	2002-07-16
*	R_sqr ne contient plus de resultats sur sqrt -> R_sqrt	desmettr	2002-07-16
*	MAJ Reals	desmettr	2002-07-16
*	MAJ Rgeom	desmettr	2002-07-16
*	Proprietes (calculatoires) des fonctions trigonometriques	desmettr	2002-07-16
*	Proprietes de la racine carree	desmettr	2002-07-16
*	Definition de la racine carree	desmettr	2002-07-16
*	code retour de make check	courant	2002-07-15
*	Pb de factorisation camlp4	herbelin	2002-07-15
*	Pour assurer une compatibilite avec la 7.3	herbelin	2002-07-15
*	Bug de précédence	herbelin	2002-07-15
*	Correction bug Tauto : la regle pour (A->B)->C echouait quand C etait	courant	2002-07-15
*	Preuve de cos_plus	desmettr	2002-07-12
*	Quelques resultats supplementaires sur les suites convergentes	desmettr	2002-07-12
*	Le theoreme central sur les produits de Cauchy finis	desmettr	2002-07-12
*	Differents resultats sur les produits finis	desmettr	2002-07-12
*	* empty log message *	desmettr	2002-07-12
*	cos_plus prouve	desmettr	2002-07-12
*	Hack pour parser '{x:T\|P}*B' sans parentheses	herbelin	2002-07-11
*	Protection contre l'encapsulage de FailError dans Exc_located (sinon, par exe...	herbelin	2002-07-11
*	Error_in_file redondant et inapproprié	herbelin	2002-07-11
*	Que la localisation des erreurs pour les tactiques atomiques marche	herbelin	2002-07-11
*	Généralisation des syntaxes ': T := t', ':= t : T', ': T', ':= t' pour	herbelin	2002-07-11