coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	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
*	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
*	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
*	Ajout syntaxe '>'	herbelin	2002-12-15
*	Pas d'associativite pour =_D	herbelin	2002-12-15
*	cond_pos -> cond_positivity pour cause de conflit avec posreal...	desmettr	2002-11-27
*	Réorganisation de la librairie des réels	desmettr	2002-11-27
*	MAJ	desmettr	2002-11-26
*	Theorie 'light' des réels	desmettr	2002-11-26
*	Explicitation de NONA car sinon LEFTA par défaut; déplacement dans 5	herbelin	2002-11-26
*	Utilisation des niveaux de camlp4 pour gérer les niveaux de constr; amélior...	herbelin	2002-11-24