coq - The formal proof system

Age	Commit message (Expand)	Author
2003-11-22	Traitement plus clair, notamment pour Locate, de quand quoter les composantes...	herbelin
2003-11-21	ajout Pnat et Pcompare_antisym	herbelin
2003-11-19	Distinction entre 'as _' qui cache le terme filtre (si variable) et rien dans...	herbelin
2003-11-18	reparation bug moins unaire (erreur de PP)	barras
2003-11-18	Mise en place systeme de qualification des noms renommes; Renommages dans Rin...	herbelin
2003-11-17	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-16	Bug filtrage pour inversion notation	herbelin
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-12	Test de la reference principale plutot que le module dans lequel se trouve la...	herbelin
2003-11-09	Quelqes renommages lies a Zorder	herbelin
2003-11-05	Nouvelle vague de renommage	herbelin
2003-11-04	Extension de zarith	herbelin
2003-11-01	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-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