coq - The formal proof system

Age	Commit message (Expand)	Author
2003-11-14	Conflit renommage	herbelin
2003-11-14	Oublis dans les rennomages	herbelin
2003-11-14	Suppression renommages dans Peano	herbelin
2003-11-13	moins unaire au niveau 35, tactiques simple_induction et simple_destruct, Loc...	barras
2003-11-12	Nouvelle et derniere vague de renommage	herbelin
2003-11-09	Quelqes renommages lies a Zorder	herbelin
2003-11-05	Nouvelle vague de renommage	herbelin
2003-11-01	Extensibilite de la grammaires des patterns	herbelin
2003-10-27	Nouveaux renommages; mot-cle 'exists'	herbelin
2003-10-21	Nouveaux renommages; Traduction speciale pour 'length nil'	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	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-10	changement nouvelle syntaxe (pt fixes)	barras
2003-09-30	Les notations hors scope s'empilent maintenant comme des scopes ne	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-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-18	Traduction de '_' comme reference	herbelin
2003-09-12	Scope type pour le codomaine de Prod aussi; ajout extern_rawtype	herbelin
2003-09-10	Renommage des variables '_'	herbelin
2003-09-10	Ajout 'mod' comme keyword	herbelin
2003-09-09	Ajout If; renommage de l'ident '_'	herbelin
2003-09-06	Paramétrisation vis à vis de existential_key	herbelin
2003-09-02	Plus de passage du scope tmp sous les lambdas	herbelin
2003-08-31	Symetrisation des changements implicites de scope	herbelin
2003-08-14	Traducteur de correctness	herbelin
2003-08-12	Bug et améliorations diverses	herbelin
2003-08-11	Nouvelle mouture du traducteur v7->v8	herbelin
2003-06-10	Amélioration afficheur de Cases pour les constr_pattern	herbelin
2003-05-19	Renommage CMeta en CPatVar qui sert à saisir les PMeta de Pattern	herbelin
2003-04-16	simplification: fst (list_chop n l) = firstn n l et snd (list_chop n l) = lis...	letouzey
2003-04-16	On force l'affichage des implicites non '?' lors de la traduction	herbelin
2003-04-15	Affichage coercions en mode -(f)translate	herbelin
2003-04-10	Affichage forcé des implicites contextuels si pas de contexte connu	herbelin
2003-04-09	Mécanisme plus simple et efficace pour traduire les implicites	herbelin
2003-04-09	Réorganisation de Impargs + mise en place d'une infrastructure	herbelin
2003-04-07	Stratégie d'affichage des coercions plus défensive (mais pas très optimale)	herbelin
2003-04-07	Suppression des explicitations d'implicite inutiles	herbelin
2003-04-01	Déplacement with_option dans Options	herbelin
2003-03-29	Mise en place de 'Implicit Variable' (variante du 'Reserve' de mizar)	herbelin
2003-03-21	correction affichage des modules	barras
2003-03-12	* empty log message *	barras
2002-12-10	Avertissement plus clair	herbelin