coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	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
*	Bug et améliorations diverses	herbelin	2003-08-12
*	Ajout LetTuple	herbelin	2003-08-11
*	Nouvelle mouture du traducteur v7->v8	herbelin	2003-08-11
*	Ajout notation c.(f) en v8 pour les projections de Record	herbelin	2003-06-10
*	Déplacement traducteur de nom dans Constrextern pour accès aux noms longs	herbelin	2003-06-10
*	Amélioration afficheur de Cases pour les constr_pattern	herbelin	2003-06-10
*	Extension de Locate sur les symboles avec recherche de sous-chaînes; mise en...	herbelin	2003-06-10
*	Suppression définitive de lmatch et or_metanum dans tacinterp	herbelin	2003-05-21
*	Fusion à l'essai de lmatch et lfun dans tacinterp; utilisation de noms pour ...	herbelin	2003-05-21
*	Renommage CMeta en CPatVar qui sert à saisir les PMeta de Pattern	herbelin	2003-05-19
*	Restructuration des procédures de filtrage	herbelin	2003-05-19
*	Hack pour ameliorer l'affichage des applications dans les `...` et	herbelin	2003-05-14
*	Prise en compte des syntaxes v8 dans Uninterpreted Notation	herbelin	2003-04-29
*	Ajout "at next level" dans Notation	herbelin	2003-04-17
*	simplification: fst (list_chop n l) = firstn n l et snd (list_chop n l) = lis...	letouzey	2003-04-16