coq - The formal proof system

Age	Commit message (Expand)	Author
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
2001-09-12	Rustine pour gérer inject_nat	herbelin
2001-09-11	Un look un peu plus avenant aux productions des règles de grammaire	herbelin
2001-09-11	Du bon usage des commentaires coqweb	herbelin
2001-09-11	Conformité des commentaires au format coqweb	herbelin
2001-09-11	MAJ	herbelin
2001-09-10	Hack pour gérer les univers dans les prédicats de Cases synthétisés	herbelin
2001-09-10	changement du make depend en vu du make reals	letouzey
2001-09-10	bug de rename_global modulaire corrige'	letouzey
2001-09-10	Utilisation d'un type spécifique (elimination_sorts) pour caractériser les ...	herbelin