coq - The formal proof system

Age	Commit message (Expand)	Author
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
2000-11-27	Ajout de evaluable_named_decl et evaluable_rel_decl en parallele au evaluable...	herbelin
2000-11-27	Affichage des définitions locales	herbelin
2000-11-27	Ajout map_constr_with_full_binders et strong pour Simpl	herbelin
2000-11-27	Changement du parseur par défaut dans Syntax	herbelin
2000-11-27	Généralisation de constant_opt_value en reference_opt_value	herbelin
2000-11-27	Branchement du mécanisme d'instantiation des Evar en présence de définitio...	herbelin
2000-11-27	Prise en compte des let-in dans les fonctions de réduction pour les tactiques	herbelin
2000-11-27	Bug dans le calcul des dépendances dans add_discharged_constant	herbelin
2000-11-26	Nettoyage	herbelin
2000-11-26	Appel des constantes globaux par des noms absolus	herbelin
2000-11-26	Le nouvel Induction s'appelle NewInduction	herbelin
2000-11-26	MAJ	herbelin
2000-11-26	Prise en compte qualid	herbelin
2000-11-26	Restruration autour de qualidarg	herbelin
2000-11-26	Calcul du chemin optimal dans qualid_of_global	herbelin