coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Modularisation des preuves concernant la logique classique, l'indiscernabilit...	herbelin	2006-03-05
*	Commentaires	herbelin	2006-03-05
*	Renommage du IP classique pour éviter confusion avec IP constructif	herbelin	2006-03-05
*	Ajout étude IP généralisé, Gödel-Dummett, buveur	herbelin	2006-03-05
*	Petite simplification en passant	herbelin	2006-03-04
*	add a left and right tactic for classical logic	narboux	2005-07-15
*	MAJ changements ChoiceFacts	herbelin	2004-12-05
*	Paramétrisation du domaine des axiomes de choix + ajout description = choice...	herbelin	2004-12-05
*	MAJ commentaire sur incohérence EM dans Set	herbelin	2004-11-07
*	Réponse à la conjecture que PI est indépendant de EM dans CC	herbelin	2004-11-02
*	Minimisation utilisation NNPP	herbelin	2004-08-03
*	Déclaration d'obsolescence	herbelin	2004-08-03
*	Typo	herbelin	2004-08-03
*	Ref	herbelin	2004-08-03
*	Commentaires coqdoc	herbelin	2004-08-01
*	Commentaires coqdoc	herbelin	2004-08-01
*	Nouvelle en-tête	herbelin	2004-07-16
*	simplified proof (eq and eqT are now the same)	barras	2004-06-25
*	eq2eqT et eqT2eq devenus obsolètes	herbelin	2004-06-02
*	MAJ commentaires	herbelin	2004-03-24
*	Commentaires	herbelin	2004-03-17
*	MAJ simplification	herbelin	2004-01-27
*	changement de pose en set (pose n'etait pas utilise avec la semantique	barras	2003-12-24
*	modif existentielle (exists \| --> exists ,) + bug d'affichage des pt fixes	barras	2003-12-15
*	Remplacement des fichiers .v ancienne syntaxe de theories, contrib et states ...	herbelin	2003-11-29
*	Biblio standard sans mention de la possibilite d'etre impredicatif	herbelin	2003-11-07
*	Biblio standard sans impredicativite	herbelin	2003-11-07
*	Preuve de l'incoherence de {A}+{~A} avec Set impredicatif	herbelin	2003-11-05
*	Cosmetique	herbelin	2003-11-02
*	Renforcement significatif du resultat principal	herbelin	2003-11-02
*	Rien de bien important	herbelin	2003-11-02
*	Commentaires	herbelin	2003-11-02
*	Typo	herbelin	2003-11-02
*	AC + EXT -> EM	herbelin	2003-11-02
*	Relations entre le choix (forme relationnelle) avec restriction ou non	herbelin	2003-11-02
*	Renommage bool en boolP pour eviter la qualification	herbelin	2003-11-02
*	Choix sous sa forme relationnelle	herbelin	2003-10-29
*	MAJ	herbelin	2003-10-28
*	Fichier offrant l'axiome du choix unique en presence de logique classique	herbelin	2003-10-28
*	Fichier offrant l'axiome du choix en presence de logique classique	herbelin	2003-10-28
*	La logique sur Type inclut celle sur Set	herbelin	2003-10-28
*	Cacher les .v8	herbelin	2003-10-03
*	Ajout ChoiceFacts	herbelin	2003-04-29
*	Blancs	herbelin	2003-04-29
*	Renommage K; equivalence JMeq et eq_dep sur Type	herbelin	2003-04-09
*	Documentation, généralisation à eq sur Type, preuves d'équivalence des	herbelin	2003-04-03
*	JMeq now treated as an equality by tactics.	courant	2002-11-14
*	Preuves dans CC de	herbelin	2002-08-13
*	Ajout Hurkens.v, ProofIrrelevances.v et l'indiscernabilite dans Classical_Prop.v	herbelin	2002-05-29
*	Uniformisation (Qed/Save et Implicits Arguments)	herbelin	2002-04-17