coq - The formal proof system

Age	Commit message (Expand)	Author
2003-11-01	Finalement, niveau 0 pour l'argument du '-' unaire, pour éviter que	herbelin
2003-11-01	Controle par le prefixe et plus par le nom absolu pour la recherche d'objets ...	herbelin
2003-11-01	Interdiction de nommer un object de nom commencant par Coq en dehors de la bi...	herbelin
2003-11-01	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	Heritage des notations v7 seulement si zero information v8	herbelin
2003-11-01	Debranchement de Print si pas verbose (necessaire pour traducteur)	herbelin
2003-10-31	maj	filliatr
2003-10-30	Redirected some of the verbose jprover output through the Pp module.	corbinea
2003-10-30	Parsing du moins unaire au niveau de l'application qui n'a pas besoin d'etre ...	herbelin
2003-10-30	Affichage des negatifs au niveau de l'application, et des positifs au dessus ...	herbelin
2003-10-30	traduction des noms de correctness	herbelin
2003-10-29	* empty log message *	herbelin
2003-10-29	Choix sous sa forme relationnelle	herbelin
2003-10-29	maj	filliatr
2003-10-28	MAJ	herbelin
2003-10-28	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-27	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-23	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-22	maj	filliatr
2003-10-22	Deplacement de iter_constr_with_full_binders dans Termops	herbelin
2003-10-22	MAJ	herbelin