coq - The formal proof system

Age	Commit message (Expand)	Author
2000-11-27	Prise en compte des définitions locales	herbelin
2000-11-27	Branchement des Local sur des SectionLocalDef	herbelin
2000-11-26	Prise en compte noms longs dans divers fonctions de Print	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	Réorganisation autour de globalize_constr	herbelin
2000-11-24	Ajout objets END-SECTION pour les nametabs + nettoyage lib/nametab	filliatr
2000-11-24	certains effets disparaissent a la sortie des sections, d'autres non (selon S...	filliatr
2000-11-24	SearchPattern et SearchRewrite	filliatr
2000-11-24	- coqc: utilise le meilleur coq possible	filliatr
2000-11-23	print_id, print_sp -> pr_id, pr_sp	herbelin
2000-11-23	Informations inutiles	herbelin
2000-11-23	print_id, print_sp -> pr_id, pr_sp	herbelin
2000-11-23	Bug qualidconstarg (intervient pour Transparent)	herbelin
2000-11-23	Reparation IsMutConstruct + Transparent	mohring
2000-11-22	Abstraction du type 'qualid' pour les noms qualifiés relatifs distinct de 's...	herbelin
2000-11-22	Nettoyage	herbelin
2000-11-22	deplacement poly_args; iterateurs sur les segments	filliatr
2000-11-22	retablissement de line_oriented_parser pour Yves	filliatr
2000-11-21	Elimination d'un test sur les macros	delahaye
2000-11-21	implicites manuels	filliatr
2000-11-21	Begin-End Silent deviennent Set?Unset Silent	mohring
2000-11-21	separation calcul des implicites et declaration des constantes / inductifs / ...	filliatr
2000-11-20	Petit bug entre close_section's	herbelin
2000-11-20	Prise en compte des noms qualifiés dans certaines commandes	herbelin
2000-11-20	Prise en compte noms longs	herbelin
2000-11-20	Tables séparées pour chaque type de global; calcul de la Nametab de la sect...	herbelin
2000-11-20	Ajout erreur GlobalNotFound	herbelin
2000-11-20	Mieux à sa place dans toplevel	herbelin
2000-11-20	Prise en compte noms longs	herbelin
2000-11-20	Une capsule pour save_module_to dans Discharge	herbelin
2000-11-15	methode export	filliatr
2000-11-10	Bugs lies a la confusion load/open et a un open abusivement recursif dans lib...	herbelin
2000-11-09	Renommage canonique SectionLocalDecl -> SectionLocalAssum	herbelin
2000-11-08	nouveau load path	filliatr
2000-11-08	amélioration	herbelin
2000-11-08	out_variable (Liboject.obj -> ...) distibgue de get_variable	filliatr
2000-11-07	Modification de la table des tactic Definitions pour eviter l'ecriture	mohring
2000-11-06	Nettoyage Names et conséquences (dont ajout d'un type dir_path, argument de ...	herbelin
2000-11-06	print_idl inliné	herbelin
2000-11-06	nouveau discharge fait par le noyau; plus de recettes dans les corps des cons...	filliatr
2000-11-03	compilation avec make de Solaris; README et INSTALL	filliatr
2000-11-02	correction Abstract (et make world passe!)	filliatr
2000-11-02	suppression des (* open Generic *)	filliatr
2000-10-30	Ajout d'un switch pour le debugger	delahaye
2000-10-27	g_natsyntax et g_zsyntax maintenant toujours linkes	filliatr
2000-10-24	Meilleur endroit pour déclarer les parseurs de grammaires et joli affichage	herbelin
2000-10-23	Rétablissement compatibilité des implicites (2ème) (mais amélioration)	herbelin
2000-10-23	Import de Infix au Require	herbelin
2000-10-23	code mort	herbelin