coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	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 notations pour les expressions dans un anneau	herbelin	2003-10-28
*	Simplification preuve	herbelin	2003-10-28
*	Ajout de Print Visibility	herbelin	2003-10-28
*	Ajout %core; MAJ niveau connecteurs logique	herbelin	2003-10-28
*	Affichage Assert_failure en ocaml 3.07	herbelin	2003-10-28
*	Message inductive large	herbelin	2003-10-28
*	Nouveaux fichiers dans Logic	herbelin	2003-10-28
*	Nouveaux fichiers dans Logic; prise en compte de l'option -strongly-classical...	herbelin	2003-10-28
*	Options -strongly-constructive et -strongly-classical	herbelin	2003-10-28
*	Set devient predicatif par defaut	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 Double Inversion	herbelin	2003-10-27
*	MAJ	herbelin	2003-10-27
*	Nouveaux renommages; mot-cle 'exists'	herbelin	2003-10-27
*	Bug du commit precedent	herbelin	2003-10-27
*	maj	filliatr	2003-10-23
*	Saut de ligne avant les infos non logiques de print_about	herbelin	2003-10-23
*	Conjecture declare maintenant un axiome; reorganisation VernacDefinition	herbelin	2003-10-23
*	Independance de grammar.cmo vis a vis de Search; reorganisation VernacDefinition	herbelin	2003-10-23
*	Independance de grammar.cmo vis a vis de Search	herbelin	2003-10-23
*	Conjecture declare maintenant un axiome; reorganisation VernacDefinition	herbelin	2003-10-23
*	Commentaires	herbelin	2003-10-23
*	Jprover bugfix (hopefully !)	corbinea	2003-10-23
*	maj	filliatr	2003-10-22
*	Deplacement de iter_constr_with_full_binders dans Termops	herbelin	2003-10-22
*	MAJ	herbelin	2003-10-22
*	Ajout NArithRing	herbelin	2003-10-22
*	Documentation/Structuration	herbelin	2003-10-22
*	Documentation/Structuration	herbelin	2003-10-22
*	MAJ	herbelin	2003-10-22
*	Suppression dependance formelle en Vernacexpr	herbelin	2003-10-22
*	Integration de SearchNamed dans SearchAbout	herbelin	2003-10-22
*	Deplacement du pr_reference du traducteur dans Ppconstrnew; integration de Se...	herbelin	2003-10-22
*	reorganisation des niveaux (ex: = est a 70)	barras	2003-10-22
*	nouvelles priorites + Hints	barras	2003-10-22
*	Deplacement de Ppvernacnew.pr_reference dans Ppconstrnew pour utilisation par...	herbelin	2003-10-21
*	Nouveaux renommages; Traduction speciale pour 'length nil'	herbelin	2003-10-21
*	Redondance de dec_eq_nat	herbelin	2003-10-21
*	Type relation dans Datatypes	herbelin	2003-10-21
*	Construction des chemins de constantes plus robuste	herbelin	2003-10-21
*	Optimisation de gen_constant_in_modules	herbelin	2003-10-21
*	Extension de Locate	herbelin	2003-10-21