coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	MAJ V7.1	herbelin	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-20
*	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-19
*	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