coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	New tactics : econstructor, eleft, eright, esplit	clrenard	2003-11-17
*	Un ident filtre est liant seulement si une variable deja liee (sinon bug dans...	herbelin	2003-11-17
*	Bug filtrage pour inversion notation	herbelin	2003-11-16
*	Conflit renommage	herbelin	2003-11-14
*	Oublis dans les rennomages	herbelin	2003-11-14
*	Suppression renommages dans Peano	herbelin	2003-11-14
*	moins unaire au niveau 35, tactiques simple_induction et simple_destruct, Loc...	barras	2003-11-13
*	Nouvelle et derniere vague de renommage	herbelin	2003-11-12
*	Test de la reference principale plutot que le module dans lequel se trouve la...	herbelin	2003-11-12
*	Quelqes renommages lies a Zorder	herbelin	2003-11-09
*	Nouvelle vague de renommage	herbelin	2003-11-05
*	Extension de zarith	herbelin	2003-11-04
*	Extensibilite de la grammaires des patterns	herbelin	2003-11-01
*	Renommage Topconstr.map_aconstr_with_binders_loc	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
*	Controle par le prefixe et plus par le nom absolu pour la recherche d'objets ...	herbelin	2003-11-01
*	Parsing du moins unaire au niveau de l'application qui n'a pas besoin d'etre ...	herbelin	2003-10-30
*	Ajout de Print Visibility	herbelin	2003-10-28
*	Nouveaux renommages; mot-cle 'exists'	herbelin	2003-10-27
*	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-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