coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	Changement de la politique de V8only: V8only tout seul signifie	herbelin	2003-09-21
\| \| \| \| \| \| \| \| \|	'seulement interprétation' en V8; héritage des paramêtres de V7 seulement si pas V8only; sinon, il faut tout expliciter (pas d'héritage partiel) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4433 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Zdiv plus efficace: r+r -> 2*r	letouzey	2003-09-05
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4308 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Ajout Open Scope	herbelin	2003-04-09
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3890 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Suppression de l'étage "Import nat/Z/R_scope". "Open Scope" remplace "Import".	herbelin	2003-04-09
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3877 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Pas d'associativité gauche au niveau 3 en vieille syntaxe !	herbelin	2003-03-28
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3803 85f007b7-540e-0410-9357-904b9bb8a0f7
*	* empty log message *	barras	2003-03-21
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3783 85f007b7-540e-0410-9357-904b9bb8a0f7
*	* empty log message *	barras	2003-03-12
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3761 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
*	affaiblissement hyp de Zmult_reg_left	filliatr	2002-06-05
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2758 85f007b7-540e-0410-9357-904b9bb8a0f7
*	encore des lemmes sur Zdiv	filliatr	2002-05-14
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2678 85f007b7-540e-0410-9357-904b9bb8a0f7
*	nouveaux lemmes dans Zdiv (Claude Marche)	filliatr	2002-05-14
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2677 85f007b7-540e-0410-9357-904b9bb8a0f7
*	lemmes sur Zdiv/Zmod	filliatr	2002-04-19
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2661 85f007b7-540e-0410-9357-904b9bb8a0f7
*	un thm de plus dans Zdiv; un retour chariot apres un message de la tactique ↵	filliatr	2002-04-19
\| \| \| \| \| \|	FourierR git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2659 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Uniformisation (Qed/Save et Implicits Arguments)	herbelin	2002-04-17
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2650 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Zdiv -> Export ZArith	filliatr	2002-04-08
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2621 85f007b7-540e-0410-9357-904b9bb8a0f7
*	syntaxe pour Zdiv et Zmod	filliatr	2002-04-08
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2620 85f007b7-540e-0410-9357-904b9bb8a0f7
*	simplification preuve	filliatr	2002-04-05
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2615 85f007b7-540e-0410-9357-904b9bb8a0f7
*	nouveau module Zdiv	filliatr	2002-04-05
	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2614 85f007b7-540e-0410-9357-904b9bb8a0f7