coq - The formal proof system

Age	Commit message (Expand)	Author
2000-11-29	Now AddRecPath and AddPath can be used with an As option to specify the	sacerdot
2000-11-29	load_path_entry structure simplified; field relative_subdir renamed to coq_dirpa	sacerdot
2000-11-29	load_path_entry structure simplified; field relative_subdir renamed to coq_dirpa	sacerdot
2000-11-29	load_path_entry structure simplified; field relative_subdir renamed to coq_di...	sacerdot
2000-11-29	mise à jour	filliatr
2000-11-29	Nouveau long long avec Coq en tête	herbelin
2000-11-29	MAJ	herbelin
2000-11-29	La zone par défaut pour le nommage des modules est Scratch	herbelin
2000-11-29	Code mort	herbelin
2000-11-29	Ajout d'une option d'alias à -I	herbelin
2000-11-29	Nouveau long long avec Coq en tête	herbelin
2000-11-29	Enregistrement des racines de la bibliothèque	herbelin
2000-11-29	Ajout d'un alias à add_path, rec_add_path et all_subdirs pour associer un ch...	herbelin
2000-11-29	Ajout d'un test pour vérifier qu'on a affaire à un ident	herbelin
2000-11-29	Déplacement du message d'erreur de gen_rel vers l'appelant pour le prétypage	herbelin
2000-11-29	Now also inner-types are exported.	sacerdot
2000-11-28	Hack pour contourner CVS en local dans la recherche rcursive de load_path	herbelin
2000-11-28	Remplacement des add_include par add_rec_include pour avoir le repertoire dan...	herbelin
2000-11-28	Les variables doivent persister dans les vo pour HELM	herbelin
2000-11-28	Code clean-up due to the new usage of longer names in Coq.	sacerdot
2000-11-28	Prise en compte du repertoire dans le section path; utilisation de dirpath po...	herbelin
2000-11-28	Ajout des Fix et CoFix dans les patterns	delahaye
2000-11-28	Added -R inclusion to fix compilation in not-local configuration.	sacerdot
2000-11-28	-I inutiles pour coqc et utilisation de -R theories (pour garder trace des no...	herbelin
2000-11-28	Elimination du '	delahaye
2000-11-28	Elimination du '	delahaye
2000-11-28	Un == non reconnu sous alpha	delahaye
2000-11-28	Rajout de PolyListSyntax aussi dans Makefile	herbelin
2000-11-27	Distinction local/global	herbelin
2000-11-27	Bug affichage inductifs	herbelin
2000-11-27	Xml contrib retached	sacerdot
2000-11-27	Many improvements. Xml contrib retached to the V7.	sacerdot
2000-11-27	uniformisation messages d'erreur	filliatr
2000-11-27	load_module / open_module un tantinet plus rapides	filliatr
2000-11-27	Faut-il mettre la réduction let-in dans la réduction unfold ?	herbelin
2000-11-27	Remettre une section dans fast_integer pour contourner un bug de définition ...	herbelin
2000-11-27	La bonne modif des Unfold	herbelin
2000-11-27	MAJ	herbelin
2000-11-27	Bug dans find_common_hyps_then_abstract en présence de défs locales	herbelin
2000-11-27	La table de pré-évaluation des constantes ne doit pas persister au discharge	herbelin
2000-11-27	Bug extract_instance en présence de défs locales	herbelin
2000-11-27	Prise en compte des définitions locales	herbelin
2000-11-27	Prise en compte des implicites de locaux à l'affichage	herbelin
2000-11-27	On déplie les locaux dans les types plutôt que de les quantifier par un Let	herbelin
2000-11-27	Suppression de Unfold inutile et maintenant échouant	herbelin
2000-11-27	Prise en compte des let-in dans les fonctions de réduction pour les tactiques	herbelin
2000-11-27	Utilisation de Let In pour les constantes locales, prise en compte des Let In...	herbelin
2000-11-27	Bug dans la gestion du contexte en présence de Fix dans le calcul de garde	herbelin
2000-11-27	Branchement des Local sur des SectionLocalDef	herbelin
2000-11-27	Prise en compte des let in dans les instances de globaux	herbelin