coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
...
*	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
*	Definition et proprietes de l'integrale de Riemann	desmettr	2002-11-18
*	Proprietes des fonctions en escalier	desmettr	2002-11-18
*	Réforme de l'interprétation des termes :	herbelin	2002-11-14
*	nettoyage preuve limit_comp	courant	2002-11-14