coq - The formal proof system

Age	Commit message (Expand)	Author
2001-09-20	Nombre magique pour la V7.1	herbelin
2001-09-20	Le prédicat du vieux Case ne doit pas contenir d'univers algébrique même q...	herbelin
2001-09-20	Report des modifs de Claudio	herbelin
2001-09-20	Pas de warning pour le -I . par défaut de Coq	herbelin
2001-09-20	bug affichage des termes ml fournis	letouzey
2001-09-20	utilisation du nouveau get_sort_family_of	letouzey
2001-09-20	changements mineurs du test	letouzey
2001-09-20	warning silencieux	filliatr
2001-09-20	version V7.1	herbelin
2001-09-20	Restriction de l'avertissement add_loadpath au mode verbeux	herbelin
2001-09-20	On ignore les répertoires qui ne correspondent pas à des idents	herbelin
2001-09-20	On ignore les répertoires invisibles dans all_subdirs	herbelin
2001-09-20	Romega	mohring
2001-09-20	let-in dans Refine	filliatr
2001-09-20	Refine et let-in	filliatr
2001-09-19	Blindage, de peur que des types entrant non en forme normale ne provoque des ...	herbelin
2001-09-19	Nouvelle fonction get_sort_family_of pour calculer la famille dans lequel vit...	herbelin
2001-09-19	Type 'sorts_family' (ex elimination_sorts) pour caractériser les familles de...	herbelin
2001-09-19	Nouvelle fonction sort_family_of pour calculer la famille dans lequel vit un ...	herbelin
2001-09-19	Intégration partielle des modifs de la V7.0	herbelin
2001-09-19	Affichage des dir_path vide	herbelin
2001-09-19	Autorisation de surcharge d'un -R par un -I	herbelin
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