coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
...
*	Correction typo eq_rec_eq (cf bug #1339)	herbelin	2007-01-31
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9567 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Derivation of (exists x : A, P x) -> {x : A \| P x} for decidable P	emakarov	2007-01-23
\| \| \| \| \| \| \| \|	and countable A. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9522 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Clarification redondance Axiome du choix unique/description	herbelin	2007-01-22
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9513 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Remplacement axiome JMeq_eq dans BinPos par eq_dec_eq sur type à	herbelin	2006-12-28
\| \| \| \| \| \| \|	égalité décidable + maj dépendances git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9467 85f007b7-540e-0410-9357-904b9bb8a0f7
*	AllÃègement de syntxe suite à l'introduction de l'unif pattern	herbelin	2006-12-12
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9439 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Mise en forme des theories	notin	2006-10-17
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9245 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Passage à une définition de inhabited plus dans les 'standard ↵	herbelin	2006-08-28
\| \| \| \| \| \|	mathématiques'; ajout preuve que tous les 'epsilon i P' sont égaux si P habité git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9093 85f007b7-540e-0410-9357-904b9bb8a0f7
*	"Essai de remplacement de "ex P" par "exists x, P x" suite à	herbelin	2006-08-28
\| \| \| \| \| \| \| \|	l'introduction d'unification de motifs à la Miller permettant une forme restreinte canonique d'unification du second ordre git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9091 85f007b7-540e-0410-9357-904b9bb8a0f7
*	JMeq maintenant applicable sur Type	herbelin	2006-08-24
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9077 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Typo	herbelin	2006-07-06
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9026 85f007b7-540e-0410-9357-904b9bb8a0f7
*	MAJ du manuel de référence	notin	2006-07-04
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8999 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Déplacement Int.v dans ZArith, déplacement de DecidableType.v et ↵	herbelin	2006-06-09
\| \| \| \| \| \|	DecidableTypeEx.v dans Logic git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8933 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Ajout exists! et restructuration/extension des fichiers sur la	herbelin	2006-06-04
\| \| \| \| \| \| \|	description et le choix git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8893 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Ajout exists! et restructuration/extension des fichiers sur la	herbelin	2006-06-04
\| \| \| \| \| \| \|	description et le choix git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8892 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Standardisation du nom des méthodes de Evd	herbelin	2006-04-28
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8759 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Suppression des fichiers .cvsignore, rendus obsolètes par le systèmes des ↵	notin	2006-04-28
\| \| \| \| \| \|	'properties' de Subversion git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8758 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Réajout de eq_rec_eq oublié lors de la modularisation de Eqdep	herbelin	2006-03-30
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8674 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Modification des propriétés (svn:executable)	notin	2006-03-17
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8642 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Modularisation des preuves concernant la logique classique, ↵	herbelin	2006-03-05
\| \| \| \| \| \|	l'indiscernabilité des preuves et l'axiome K git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8136 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Commentaires	herbelin	2006-03-05
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8135 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Renommage du IP classique pour éviter confusion avec IP constructif	herbelin	2006-03-05
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8132 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Ajout étude IP généralisé, Gödel-Dummett, buveur	herbelin	2006-03-05
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8131 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Petite simplification en passant	herbelin	2006-03-04
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8122 85f007b7-540e-0410-9357-904b9bb8a0f7
*	add a left and right tactic for classical logic	narboux	2005-07-15
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7234 85f007b7-540e-0410-9357-904b9bb8a0f7
*	MAJ changements ChoiceFacts	herbelin	2004-12-05
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6401 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Paramétrisation du domaine des axiomes de choix + ajout description = ↵	herbelin	2004-12-05
\| \| \| \| \| \|	choice pour les propriétés décidables vers nat git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6399 85f007b7-540e-0410-9357-904b9bb8a0f7
*	MAJ commentaire sur incohérence EM dans Set	herbelin	2004-11-07
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6281 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Réponse à la conjecture que PI est indépendant de EM dans CC	herbelin	2004-11-02
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6273 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Minimisation utilisation NNPP	herbelin	2004-08-03
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6012 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Déclaration d'obsolescence	herbelin	2004-08-03
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6011 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Typo	herbelin	2004-08-03
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6010 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Ref	herbelin	2004-08-03
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6009 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Commentaires coqdoc	herbelin	2004-08-01
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6004 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Commentaires coqdoc	herbelin	2004-08-01
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6001 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Nouvelle en-tête	herbelin	2004-07-16
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5920 85f007b7-540e-0410-9357-904b9bb8a0f7
*	simplified proof (eq and eqT are now the same)	barras	2004-06-25
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5824 85f007b7-540e-0410-9357-904b9bb8a0f7
*	eq2eqT et eqT2eq devenus obsolètes	herbelin	2004-06-02
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5794 85f007b7-540e-0410-9357-904b9bb8a0f7
*	MAJ commentaires	herbelin	2004-03-24
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5556 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Commentaires	herbelin	2004-03-17
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5512 85f007b7-540e-0410-9357-904b9bb8a0f7
*	MAJ simplification	herbelin	2004-01-27
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5254 85f007b7-540e-0410-9357-904b9bb8a0f7
*	changement de pose en set (pose n'etait pas utilise avec la semantique	barras	2003-12-24
\| \| \| \| \| \| \| \|	documentee). Reste a retablir la semantique de pose. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5141 85f007b7-540e-0410-9357-904b9bb8a0f7
*	modif existentielle (exists \| --> exists ,) + bug d'affichage des pt fixes	barras	2003-12-15
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5099 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Remplacement des fichiers .v ancienne syntaxe de theories, contrib et states ↵	herbelin	2003-11-29
\| \| \| \| \| \|	par les fichiers nouvelle syntaxe git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5027 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Biblio standard sans mention de la possibilite d'etre impredicatif	herbelin	2003-11-07
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4823 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Biblio standard sans impredicativite	herbelin	2003-11-07
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4822 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Preuve de l'incoherence de {A}+{~A} avec Set impredicatif	herbelin	2003-11-05
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4808 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Cosmetique	herbelin	2003-11-02
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4780 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Renforcement significatif du resultat principal	herbelin	2003-11-02
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4779 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Rien de bien important	herbelin	2003-11-02
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4778 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Commentaires	herbelin	2003-11-02
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4777 85f007b7-540e-0410-9357-904b9bb8a0f7