coq - The formal proof system

Age	Commit message (Expand)	Author
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
2000-11-26	Distinction claire entre Induction (nom interne : raw_induct) et le nouvel in...	herbelin
2000-11-26	Prise en compte noms longs dans divers fonctions de Print	herbelin
2000-11-26	Prise en compte de noms absolus dans la nametab + nettoyage	herbelin
2000-11-26	Prise en compte de noms absolus dans la nametab	herbelin
2000-11-26	Remplacement de certains sp_of_id par des locate	herbelin
2000-11-26	sp au lieu de id dans END-SECTION	herbelin
2000-11-24	MAJ	herbelin
2000-11-24	Bug relocation des hypothèses quand les contextes de définitions et d'utili...	herbelin
2000-11-24	Réorganisation autour de globalize_constr	herbelin