coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	* empty log message *	corbinea	2002-07-05
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2839 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Added a new uncompleteness bug found in Tauto.	corbinea	2002-07-05
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2838 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Hack pour autoriser les $n dans les Grammar tactic	herbelin	2002-07-03
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2837 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
*	reparation pretyping ROldCase dans le cas let	filliatr	2002-07-02
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2829 85f007b7-540e-0410-9357-904b9bb8a0f7
*	factorisation code dans make_dep_of_undep	filliatr	2002-07-02
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2827 85f007b7-540e-0410-9357-904b9bb8a0f7
*	maj	filliatr	2002-07-02
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2826 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
*	* empty log message *	desmettr	2002-07-01
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2817 85f007b7-540e-0410-9357-904b9bb8a0f7
*	* empty log message *	desmettr	2002-07-01
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2816 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
*	resynchronisation du .depend.coq	letouzey	2002-06-28
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2810 85f007b7-540e-0410-9357-904b9bb8a0f7
*	* empty log message *	mohring	2002-06-26
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2809 85f007b7-540e-0410-9357-904b9bb8a0f7
*	* empty log message *	mohring	2002-06-26
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2808 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Resolution de bug (du a Auto; remplacement par lt_O_Sn)	mayero	2002-06-26
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2807 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Integration de Rcomplet et Alembert_compl	desmettr	2002-06-25
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2806 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Integration de Rcomplet et Alembert_compl	desmettr	2002-06-25
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2805 85f007b7-540e-0410-9357-904b9bb8a0f7
*	* empty log message *	desmettr	2002-06-25
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2804 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Suppression de l'axiome d'extensionnalite	desmettr	2002-06-21
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2803 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Export Sumbool dans ProbBool; Reals charge et exporte ZArith_base seulement	filliatr	2002-06-21
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2802 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Nouvelle version avec INR + Amelioration de Sup0.	mayero	2002-06-20
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2801 85f007b7-540e-0410-9357-904b9bb8a0f7
*	* empty log message *	desmettr	2002-06-20
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2800 85f007b7-540e-0410-9357-904b9bb8a0f7
*	maj	filliatr	2002-06-20
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2799 85f007b7-540e-0410-9357-904b9bb8a0f7
*	ZArith_base, Zbool, Bool_nat	filliatr	2002-06-20
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2798 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Reparation de ring pour les setoides	clrenard	2002-06-19
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2797 85f007b7-540e-0410-9357-904b9bb8a0f7
*	ProgWf -> Zwf	filliatr	2002-06-19
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2796 85f007b7-540e-0410-9357-904b9bb8a0f7
*	deplacement contrib/correctness/ProgWf -> theories/ZArith/Zwf	filliatr	2002-06-19
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2795 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Coercion de la syntaxe des motifs non atomiques	herbelin	2002-06-19
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2794 85f007b7-540e-0410-9357-904b9bb8a0f7
*	coq_makefile utilise maintenant coqdoc	filliatr	2002-06-18
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2793 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Suppression de fct_eq	desmettr	2002-06-17
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2792 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Prise en compte de exp, cosh et sinh	desmettr	2002-06-17
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2791 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Modifications relatives a l'ajout de Rtrigo_def	desmettr	2002-06-17
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2790 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Definitions de exp, cos et sin	desmettr	2002-06-17
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2789 85f007b7-540e-0410-9357-904b9bb8a0f7
*	* empty log message *	desmettr	2002-06-17
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2788 85f007b7-540e-0410-9357-904b9bb8a0f7
*	* empty log message *	herbelin	2002-06-14
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2787 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Commentaires	herbelin	2002-06-14
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2786 85f007b7-540e-0410-9357-904b9bb8a0f7
*	* empty log message *	herbelin	2002-06-14
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2785 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Bug non vérification non redondance par Cut	herbelin	2002-06-13
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2784 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Nouvelle version de l'algorithme de compilation du filtrage compatible avec ↵	herbelin	2002-06-13
\| \| \| \| \| \|	une forme expansée des Cases git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2783 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Test de l'interprétation des fermetures de Match Context (2ème)	herbelin	2002-06-13
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2782 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Ajout map_inductive_type et map_ind_family	herbelin	2002-06-13
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2781 85f007b7-540e-0410-9357-904b9bb8a0f7