coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Independance vis a vis noms variables liees; partie sur bool dans Zbool	herbelin	2003-11-12
*	Noms/énoncés plus canoniques	herbelin	2003-11-12
*	Independance vis a vis noms variables liees	herbelin	2003-11-12
*	Ajout lemmes; independance vis a vis noms variables liees; restructuration	herbelin	2003-11-12
*	Ajout partie sur bool anciennement dans Zmisc	herbelin	2003-11-12
*	Ajout lemmes; independance vis a vis noms variables liees	herbelin	2003-11-12
*	On sait jamais	herbelin	2003-11-12
*	petits changements de syntaxe	barras	2003-11-12
*	Ajout quelques lemmes; noms des variables liees	herbelin	2003-11-09
*	Oubli BinNat	herbelin	2003-11-07
*	Oubli d'un Set Implicit Arguments	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-07
*	Des oublis	herbelin	2003-11-06
*	Report des definitions sorties de fast_integer pour compatibilite	herbelin	2003-11-06
*	Notations	herbelin	2003-11-05
*	Ajout répertoire NArith pour l'arithmétique binaire sur les nombres positif...	herbelin	2003-11-05
*	Preuve de l'incoherence de {A}+{~A} avec Set impredicatif	herbelin	2003-11-05
*	Redondances	herbelin	2003-11-05
*	Restructuration ZArith et déport de la partie sur 'positive' dans NArith, de...	herbelin	2003-11-05
*	Exporting ^; utilisation arg scope implicite	herbelin	2003-11-03
*	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
*	Restauration preference Rge a Rle pour compatibilite...	herbelin	2003-11-02
*	Restauration preference Rge a Rle pour compatibilite...; petit nettoyage	herbelin	2003-11-02
*	Finalement, niveau 0 pour l'argument du '-' uniare, pour eviter que les entie...	herbelin	2003-11-01
*	Finalement, niveau 0 pour l'argument du '-' uniare, pour eviter que les entie...	herbelin	2003-11-01
*	Parsing du moins unaire au niveau de l'application qui n'a pas besoin d'etre ...	herbelin	2003-10-30
*	Choix sous sa forme relationnelle	herbelin	2003-10-29
*	Ordre (symbolique) des Require	herbelin	2003-10-28
*	Passage de la notations de paire dans core_scope	herbelin	2003-10-28
*	Passage des notations de type dans type_scope	herbelin	2003-10-28
*	Ajout %core; MAJ niveau connecteurs logique	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-28
*	Retour en arriere sur d'autres renommages de variables	herbelin	2003-10-28
*	Retour a un nommage non standard des variables pour compatibilite; report 're...	herbelin	2003-10-27
*	Bug du commit precedent	herbelin	2003-10-27
*	Commentaires	herbelin	2003-10-23
*	Documentation/Structuration	herbelin	2003-10-22
*	Documentation/Structuration	herbelin	2003-10-22
*	reorganisation des niveaux (ex: = est a 70)	barras	2003-10-22