coq - The formal proof system

Age	Commit message (Expand)	Author
2001-09-19	ajout du fichier CHANGES	letouzey
2001-09-19	la cible all était incomplète	filliatr
2001-09-19	Protection hd d'une liste vide	herbelin
2001-09-19	adaptation a la nouvelle syntaxe Extract Inlined Constant	letouzey
2001-09-19	Changements de Extraction truc et Recursive Extraction	letouzey
2001-09-19	make install dans coq_makefile et repertoire associe user-contrib ajoute au l...	filliatr
2001-09-19	Ajout de la profondeur de section à DischargeAt pour gérer l'«open» et le...	herbelin
2001-09-19	Quelques signes extérieurs de la sémantique de Remark, question visibilité	herbelin
2001-09-19	Ces fichiers décrivent des comportements peut-être souhaités mais actuelle...	herbelin
2001-09-19	Comportements peut-être souhaités mais en tout cas non officiellement pris ...	herbelin
2001-09-19	Deux nouvelles optimisations pour Cases	letouzey
2001-09-19	MAJ V7.1	herbelin
2001-09-19	Deplacement des setoides.	clrenard
2001-09-19	Verification supplementaire avant optimisation singleton	letouzey
2001-09-19	Typo	herbelin
2001-09-19	reparation Zne	mohring
2001-09-18	Tentative de canonisation des répertoires physiques	herbelin
2001-09-18	Mise en place de noms contenant la section pour Fact et Remark	herbelin
2001-09-18	travail sur le Extract Constant	letouzey
2001-09-18	Quelques heuristiques pour gérer des représentations similaires de paths sy...	herbelin
2001-09-18	Ajout d'une option et d'une fonction compile pour fabriquer les .vo	herbelin
2001-09-18	update sur les tactiques	mayero
2001-09-18	Modification de l'emplacement des fichiers pour les setoides.	clrenard
2001-09-18	Suppression du message d'erreur si une coercion mettant en jeu des locaux n'e...	herbelin
2001-09-18	Romega/names/Makefile	mohring
2001-09-18	Bug discharge d'une déclaration de coercion pour une constante non définie ...	herbelin
2001-09-18	Modif pour Ltac et ajout de Field	delahaye
2001-09-18	modif test const	mayero
2001-09-17	Blindage de Show Intro	letouzey
2001-09-17	unification avec TOUS les sous-termes ( (plus ?) ne s'unifiait pas avec les	barras
2001-09-17	quotation des noms de fichiers pour eviter une mauvaise interpretation des \	barras
2001-09-14	MAJ	herbelin
2001-09-14	Search prenait en compte le contenu des sections alors que celui-ci n'existe ...	herbelin
2001-09-14	MAJ vis à vis de la nouvelle non-localité des Remark/Fact	herbelin
2001-09-14	Correction confusion VarNode/SectionVarNode (d'où bug Hints Unfold nom_local)	herbelin
2001-09-14	Transformation de Remark/Fact en constantes non visibles sans qualification	herbelin
2001-09-14	Ajout syntaxe "Assert H:T."	herbelin
2001-09-14	L'instantiation des evars quand un produit ou une sorte étaient attendus n'�...	herbelin
2001-09-14	L'instantiation des evars quand un produit ou une sorte étaient attendus n'�...	herbelin
2001-09-14	exceptions	barras
2001-09-14	mauvais rattrapage d'exception	barras
2001-09-13	Only CHANGES !	herbelin
2001-09-13	Structuration et traduction	herbelin
2001-09-13	Prise en compte qualid dans Hint Unfold	herbelin
2001-09-13	Syntaxe des Hints	herbelin
2001-09-13	uniformité des cibles pour les contribs	filliatr
2001-09-13	mise à jour	filliatr
2001-09-13	eclaircissement du code	courant
2001-09-13	explications modifications Tauto	courant
2001-09-12	* empty log message *	mohring