coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	Preuves dans CC de	herbelin	2002-08-13
\| \| \| \| \| \| \| \| \| \| \| \| \|	dégénérescence des propositions <-> tiers-exclu /\ extensionnalité propositionnelle et dans CCI de extensionnalité propositionnelle -> indiscernabilité des preuves git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2960 85f007b7-540e-0410-9357-904b9bb8a0f7
*	MAJ pour TAF	desmettr	2002-07-31
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2950 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Theoreme des accroissements finis generalises et corollaires	desmettr	2002-07-31
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2948 85f007b7-540e-0410-9357-904b9bb8a0f7
*	MAJ pour Exp_prop	desmettr	2002-07-31
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2946 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Proprietes de l'exponentielle	desmettr	2002-07-31
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2945 85f007b7-540e-0410-9357-904b9bb8a0f7
*	MAJ pour Rtrigo_reg	desmettr	2002-07-29
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2934 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Regularite de sin et cos	desmettr	2002-07-29
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2933 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Continuite des series de fonctions NC	desmettr	2002-07-29
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2932 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Quelques ameliorations dans Reg	desmettr	2002-07-22
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2907 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Nvll preuves R_dist_tri et tech_limit	mayero	2002-07-19
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2906 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Regularites de pow et des sommes finies / MAJ Reg	desmettr	2002-07-19
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2904 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Resultats de regularite de Rabsolu / MAJ de Reg	desmettr	2002-07-19
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2903 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Quelques ameliorations...	desmettr	2002-07-19
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2902 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Correction d'un bug dans IsCont_pt	desmettr	2002-07-18
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2899 85f007b7-540e-0410-9357-904b9bb8a0f7
*	MAJ pour Sqrt_reg	desmettr	2002-07-18
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2898 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Preuves de la continuite/derivabilite de sqrt sur R+/R+*	desmettr	2002-07-18
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2897 85f007b7-540e-0410-9357-904b9bb8a0f7
*	* empty log message *	desmettr	2002-07-16
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2884 85f007b7-540e-0410-9357-904b9bb8a0f7
*	* empty log message *	desmettr	2002-07-16
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2883 85f007b7-540e-0410-9357-904b9bb8a0f7
*	MAJ Rtrigo pour sqrt	desmettr	2002-07-16
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2880 85f007b7-540e-0410-9357-904b9bb8a0f7
*	* empty log message *	desmettr	2002-07-16
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2879 85f007b7-540e-0410-9357-904b9bb8a0f7
*	R_sqr ne contient plus de resultats sur sqrt -> R_sqrt	desmettr	2002-07-16
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2878 85f007b7-540e-0410-9357-904b9bb8a0f7
*	MAJ Reals	desmettr	2002-07-16
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2877 85f007b7-540e-0410-9357-904b9bb8a0f7
*	MAJ Rgeom	desmettr	2002-07-16
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2876 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Proprietes (calculatoires) des fonctions trigonometriques	desmettr	2002-07-16
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2875 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Proprietes de la racine carree	desmettr	2002-07-16
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2874 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Definition de la racine carree	desmettr	2002-07-16
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2873 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Bug de précédence	herbelin	2002-07-15
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2869 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Preuve de cos_plus	desmettr	2002-07-12
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2863 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Quelques resultats supplementaires sur les suites convergentes	desmettr	2002-07-12
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2862 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Le theoreme central sur les produits de Cauchy finis	desmettr	2002-07-12
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2861 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Differents resultats sur les produits finis	desmettr	2002-07-12
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2860 85f007b7-540e-0410-9357-904b9bb8a0f7
*	cos_plus prouve	desmettr	2002-07-12
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2858 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Hack pour parser '{x:T\|P}*B' sans parentheses	herbelin	2002-07-11
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2857 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Making the sumbool functions transparent, so that they can used to	bertot	2002-07-09
\| \| \| \| \| \| \|	compute even inside Coq. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2846 85f007b7-540e-0410-9357-904b9bb8a0f7
*	certains lemmes sont maintenant dans Rtrigo	desmettr	2002-07-05
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2844 85f007b7-540e-0410-9357-904b9bb8a0f7
*	sin_plus prouve (a partir de cos_plus)	desmettr	2002-07-05
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2843 85f007b7-540e-0410-9357-904b9bb8a0f7
*	sin_bound et cos_bound deplaces dans Rtrigo_alt	desmettr	2002-07-05
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2842 85f007b7-540e-0410-9357-904b9bb8a0f7
*	sin_bound et cos_bound sont prouves (merci les series alternees...)	desmettr	2002-07-05
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2841 85f007b7-540e-0410-9357-904b9bb8a0f7
*	* empty log message *	desmettr	2002-07-03
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2836 85f007b7-540e-0410-9357-904b9bb8a0f7
*	sin_eq_0 est maintenant prouve	desmettr	2002-07-03
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2835 85f007b7-540e-0410-9357-904b9bb8a0f7
*	sin_lb_gt_0 est maintenant prouve (grace a une approximation de PI, cf PI_ineq)	desmettr	2002-07-02
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2830 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Suppression de l'axiome arc_sin_cos	desmettr	2002-07-02
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2823 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Modification de IAF, introduction de TAF et preuves de 3 axiomes	desmettr	2002-07-02
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2822 85f007b7-540e-0410-9357-904b9bb8a0f7
*	* empty log message *	desmettr	2002-07-02
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2821 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Constructions des séries alternées et de PI	desmettr	2002-07-01
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2819 85f007b7-540e-0410-9357-904b9bb8a0f7
*	PI n'est plus un axiome	desmettr	2002-07-01
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2818 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Version plus propre de Rsigma	desmettr	2002-07-01
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2815 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Ajout de Binome	desmettr	2002-07-01
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2814 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Formule du binome (pour cos(x+y), sin(x+y)...)	desmettr	2002-07-01
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2813 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Modification sin_approx	desmettr	2002-07-01
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2812 85f007b7-540e-0410-9357-904b9bb8a0f7