coq - The formal proof system

Age	Commit message (Expand)	Author
2003-11-01	Ajout CPatNotation; renommage map_aconstr_with_binders_loc	herbelin
2003-11-01	Controle par le prefixe et plus par le nom absolu pour la recherche d'objets ...	herbelin
2003-10-30	Parsing du moins unaire au niveau de l'application qui n'a pas besoin d'etre ...	herbelin
2003-10-28	Ajout de Print Visibility	herbelin
2003-10-27	Nouveaux renommages; mot-cle 'exists'	herbelin
2003-10-21	Nouveaux renommages; Traduction speciale pour 'length nil'	herbelin
2003-10-21	Optimisation de gen_constant_in_modules	herbelin
2003-10-21	Bug Locate Notation	herbelin
2003-10-17	Re-desactivation de l'affichage des projections	herbelin
2003-10-16	print_projections a true juste pour le bench nocturne	herbelin
2003-10-16	Message d'erreur	herbelin
2003-10-16	Debranchement de l'affichage systematique des projections avec la notation po...	herbelin
2003-10-16	Debranchement de l'affichage systematique des projections avec la notation po...	herbelin
2003-10-15	Gestion encore plus affinee des implicites	herbelin
2003-10-14	Gestion affinee des implicites	herbelin
2003-10-14	Nouvelles traductions de noms; mot-cle; affichage implicites par le traducteur	herbelin
2003-10-14	identityT = identity	herbelin
2003-10-14	Plus d'uniformite dans la gestion des implicites d'inductifs; nouvelles entre...	herbelin
2003-10-10	identity est equivalent sur Type (sauf sans argument)	herbelin
2003-10-10	changement nouvelle syntaxe (pt fixes)	barras
2003-10-08	Pb residuel avec la prise en compte des parametres implicites d'inductifs	herbelin
2003-10-08	Prise en compte des paramètres implicites d'inductifs pour la globalisation ...	herbelin
2003-10-07	Correction du bug 335 et Export/Require Export dans un module	coq
2003-10-01	cosmetique	herbelin
2003-09-30	Les notations hors scope s'empilent maintenant comme des scopes ne	herbelin
2003-09-30	code mort	herbelin
2003-09-30	Ajout 'Close Scope'.	herbelin
2003-09-29	Prise en compte d'un inductif sans argument dans le 'in' des 'match'	herbelin
2003-09-26	Syntaxe plus liberale pour le type des arguments de filtrage du 'match'	herbelin
2003-09-26	Syntaxe plus liberale pour le type des arguments de filtrage du 'match'; trad...	herbelin
2003-09-26	Nouvelle serie de traductions	herbelin
2003-09-26	Un peu plus de souplesse dans la globalisation des noms utilises par les tact...	herbelin
2003-09-26	Decouplage printing en v8 pour les interpretations de notations	herbelin
2003-09-23	Changement de l'afficheur pour que les variables liées aient un nom indépen...	herbelin
2003-09-22	traducteur: affiche les commentaires a l'interieur des commandes	barras
2003-09-22	Bug d'externalisation des constantes avec uniquement des implicites	herbelin
2003-09-21	Mise en place d'implicites par noms en v8	herbelin
2003-09-21	Changement de la politique de V8only: V8only tout seul signifie	herbelin
2003-09-21	Mise en place d'implicites par noms en v8	herbelin
2003-09-19	parsing	herbelin
2003-09-18	Traduction de '_' comme reference	herbelin
2003-09-18	Parsing correct des explicites en cas de projection	herbelin
2003-09-12	Activation déclaration automatique de scope d'arguments; affichage scopes d'...	herbelin
2003-09-12	Activation déclaration automatique de scope d'arguments	herbelin
2003-09-12	Scope type pour le codomaine de Prod aussi; ajout extern_rawtype	herbelin
2003-09-12	Scope type pour le codomaine de Prod aussi	herbelin
2003-09-12	open superflu	herbelin
2003-09-10	Renommage des variables '_'	herbelin
2003-09-10	Ajout 'mod' comme keyword	herbelin
2003-09-09	Ajout construction If primitive dans constr_expr et rawconstr	herbelin