coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
...
*	Extensibilite de la grammaires des patterns	herbelin	2003-11-01
*	Renommage Topconstr.map_aconstr_with_binders_loc	herbelin	2003-11-01
*	Fusion de l'univers et du nom d'entree en un 'Print Grammar entry' en v8	herbelin	2003-11-01
*	Il ne faut pas mettre le constrarg des tactiques au niveau lconstr	herbelin	2003-11-01
*	Extensibilite de la grammaires des patterns	herbelin	2003-11-01
*	Traduction des noms pour les refs de pr_glob_generic (via pr_global)	herbelin	2003-11-01
*	Utilisation de niveaux pour l'extensibilite de la grammaires des patterns	herbelin	2003-11-01
*	Extension de get_constr_entry et symbol_of_production pour gerer les extensio...	herbelin	2003-11-01
*	Pas de defaut a 1 et LeftA pour les infixes v8; fusion de l'univers et du nom...	herbelin	2003-11-01
*	Ajout notations pour motifs de Cases; renommage map_aconstr_with_binders_loc	herbelin	2003-11-01
*	Ajout CPatNotation; renommage map_aconstr_with_binders_loc	herbelin	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-11-01
*	maj	filliatr	2003-10-31
*	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-30
*	* empty log message *	herbelin	2003-10-29
*	Choix sous sa forme relationnelle	herbelin	2003-10-29
*	maj	filliatr	2003-10-29
*	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-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