coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	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
*	Prise en compte des dependances dans la tactique Case	mohring	2002-03-26
*	option -dump-glob pour coqdoc	filliatr	2002-02-14
*	Protection des commentaires pour coqtex et coqweb	herbelin	2001-08-13
*	Expérimentation de NewDestruct et parfois NewInduction	herbelin	2001-08-05
*	Ajout du paradoxe de Berardi dans Logic (preuve que EM => PI dans CCI)	barras	2001-06-18
*	Mise de (*i autour CVS info	mohring	2001-04-19
*	Ajout de l'egalite de John Major	mohring	2001-04-12
*	documentation automatique de la bibliothèque standard	filliatr	2001-04-11
*	Ajout lemmes arithmetiques	mohring	2001-04-08
*	entetes	filliatr	2001-03-15
*	Renommage des variables dans les schémas d'induction	herbelin	2001-02-14
*	caractere opaque des constantes repris en compte	filliatr	2000-12-04
*	Un usage en moins de l'axiome eq_rec_eq	herbelin	2000-10-06
*	Commit malencontreux sur précédente version	herbelin	2000-10-04
*	Mise en conformité nouveau Simpl pour Fix	herbelin	2000-10-04
*	Eqdep_dec retrouve ses noms d'origine grace au nouvel Reduction.instance util...	herbelin	2000-03-21
*	Syntactic Definition n'etaient pas correctemenet importees	filliatr	2000-03-16