coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Bug Locate Notation	herbelin	2003-10-21
*	Re-desactivation de l'affichage des projections	herbelin	2003-10-17
*	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-16
*	Gestion encore plus affinee des implicites	herbelin	2003-10-15
*	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-14
*	identity est equivalent sur Type (sauf sans argument)	herbelin	2003-10-10
*	changement nouvelle syntaxe (pt fixes)	barras	2003-10-10
*	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-08
*	Correction du bug 335 et Export/Require Export dans un module	coq	2003-10-07
*	cosmetique	herbelin	2003-10-01
*	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-30
*	Prise en compte d'un inductif sans argument dans le 'in' des 'match'	herbelin	2003-09-29
*	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-26
*	Changement de l'afficheur pour que les variables liées aient un nom indépen...	herbelin	2003-09-23
*	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-22
*	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-21
*	parsing	herbelin	2003-09-19
*	Traduction de '_' comme reference	herbelin	2003-09-18
*	Parsing correct des explicites en cas de projection	herbelin	2003-09-18
*	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-12
*	Renommage des variables '_'	herbelin	2003-09-10
*	Ajout 'mod' comme keyword	herbelin	2003-09-10
*	Ajout construction If primitive dans constr_expr et rawconstr	herbelin	2003-09-09
*	Ajout If; synchro avec constrextern	herbelin	2003-09-09
*	Ajout If; renommage de l'ident '_'	herbelin	2003-09-09
*	Paramétrisation vis à vis de existential_key	herbelin	2003-09-06
*	cosmetique	herbelin	2003-09-06
*	Plus de passage du scope tmp sous les lambdas	herbelin	2003-09-02
*	Symetrisation des changements implicites de scope	herbelin	2003-08-31
*	Traducteur de correctness	herbelin	2003-08-14