coq - The formal proof system

Age	Commit message (Expand)	Author
2005-07-15	add a left and right tactic for classical logic	narboux
2004-12-05	MAJ changements ChoiceFacts	herbelin
2004-12-05	Paramétrisation du domaine des axiomes de choix + ajout description = choice...	herbelin
2004-11-07	MAJ commentaire sur incohérence EM dans Set	herbelin
2004-11-02	Réponse à la conjecture que PI est indépendant de EM dans CC	herbelin
2004-08-03	Minimisation utilisation NNPP	herbelin
2004-08-03	Déclaration d'obsolescence	herbelin
2004-08-03	Typo	herbelin
2004-08-03	Ref	herbelin
2004-08-01	Commentaires coqdoc	herbelin
2004-08-01	Commentaires coqdoc	herbelin
2004-07-16	Nouvelle en-tête	herbelin
2004-06-25	simplified proof (eq and eqT are now the same)	barras
2004-06-02	eq2eqT et eqT2eq devenus obsolètes	herbelin
2004-03-24	MAJ commentaires	herbelin
2004-03-17	Commentaires	herbelin
2004-01-27	MAJ simplification	herbelin
2003-12-24	changement de pose en set (pose n'etait pas utilise avec la semantique	barras
2003-12-15	modif existentielle (exists \| --> exists ,) + bug d'affichage des pt fixes	barras
2003-11-29	Remplacement des fichiers .v ancienne syntaxe de theories, contrib et states ...	herbelin
2003-11-07	Biblio standard sans mention de la possibilite d'etre impredicatif	herbelin
2003-11-07	Biblio standard sans impredicativite	herbelin
2003-11-05	Preuve de l'incoherence de {A}+{~A} avec Set impredicatif	herbelin
2003-11-02	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-10-29	Choix sous sa forme relationnelle	herbelin
2003-10-28	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-03	Cacher les .v8	herbelin
2003-04-29	Ajout ChoiceFacts	herbelin
2003-04-29	Blancs	herbelin
2003-04-09	Renommage K; equivalence JMeq et eq_dep sur Type	herbelin
2003-04-03	Documentation, généralisation à eq sur Type, preuves d'équivalence des	herbelin
2002-11-14	JMeq now treated as an equality by tactics.	courant
2002-08-13	Preuves dans CC de	herbelin
2002-05-29	Ajout Hurkens.v, ProofIrrelevances.v et l'indiscernabilite dans Classical_Prop.v	herbelin
2002-04-17	Uniformisation (Qed/Save et Implicits Arguments)	herbelin
2002-03-26	Prise en compte des dependances dans la tactique Case	mohring
2002-02-14	option -dump-glob pour coqdoc	filliatr
2001-08-13	Protection des commentaires pour coqtex et coqweb	herbelin
2001-08-05	Expérimentation de NewDestruct et parfois NewInduction	herbelin
2001-06-18	Ajout du paradoxe de Berardi dans Logic (preuve que EM => PI dans CCI)	barras