coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	* empty log message *	barras	2003-03-12
*	Restructuration des hints pour qu'Auto fasse moins de détours et les	herbelin	2003-02-27
*	Ajout du theoreme de Cesaro	desmettr	2003-02-14
*	Modifications dans une tactique toplevel	delahaye	2003-02-13
*	Pb de parenthèse dans "Check (S (plus O O))"	herbelin	2003-01-30
*	MAJ pour Reg	desmettr	2003-01-28
*	Documentation du contenu de REALS	desmettr	2003-01-22
*	Modifications dans SeqProp	desmettr	2003-01-22
*	Renommages dans Rtrigo_def	desmettr	2003-01-22
*	Commentaires	desmettr	2003-01-22
*	Renommages nombreux	desmettr	2003-01-22
*	Commentaires	desmettr	2003-01-22
*	Renommage f_pos -> IVT (Intermediate Value Theorem	desmettr	2003-01-22
*	Suppression d'un Import R_scope probablement oublie	desmettr	2003-01-22
*	Commentaires	desmettr	2003-01-22
*	Renommages dans RList	desmettr	2003-01-22
*	MAJ pour renommage Rcomplet	desmettr	2003-01-22
*	Renommages dans Rcomplete	desmettr	2003-01-22
*	Renommage Rcomplet.v -> Rcomplete.v	desmettr	2003-01-22
*	Suppression de lemmes superflus	desmettr	2003-01-22
*	Commentaires	desmettr	2003-01-22
*	Renommages dans PartSum	desmettr	2003-01-22
*	Bug precedence	herbelin	2003-01-22
*	Adaptation à la nouvelle sémantique plus uniforme de "Match term"	herbelin	2003-01-21
*	Renommage dans MVT	desmettr	2003-01-21
*	MAJ dans Exp_prop	desmettr	2003-01-21
*	Renommage dans Binomial.v	desmettr	2003-01-21
*	Binome.v -> Binomial.v	desmettr	2003-01-21
*	MAJ ArithProp	desmettr	2003-01-21
*	Renommage dans AltSeries.v	desmettr	2003-01-21
*	Renommage dans Alembert.v	desmettr	2003-01-21
*	Quelques améliorations	desmettr	2003-01-21
*	Suppression de INR2 / Conséquence logique de la nouvelle représentation des...	desmettr	2003-01-21
*	Quelques optimisations...	desmettr	2003-01-21
*	Cgt définition de plat	desmettr	2003-01-20
*	Amélioration de DiscrR	desmettr	2003-01-20
*	Utilisation de 'Recursive' pour les tactiques récursives	herbelin	2003-01-20
*	Utilisation de 'Recursive' pour les tactiques récursives	herbelin	2003-01-20
*	Clear sur hypothese non definie	herbelin	2003-01-19
*	Optimisations pour Sup et RCompute	desmettr	2003-01-17
*	Ajout de RCompute	desmettr	2003-01-16
*	Ajout de la tactique Sup	desmettr	2003-01-16
*	renommage de TAF.v en MVT.v	desmettr	2003-01-16
*	Correction d'un petit bug dans Sup0	desmettr	2003-01-16
*	Renommage de RealsB en Rbase	desmettr	2003-01-16
*	Renommage de Rbase.v en RIneq.v	desmettr	2003-01-16
*	Nouvelle interprétation des nombres réels	desmettr	2003-01-15
*	bit vectors	filliatr	2003-01-06
*	Re-installation nombres dans les motifs sur Z	herbelin	2002-12-28
*	Une entrée spéciale "annot" pour les piquants	herbelin	2002-12-15