coq - The formal proof system

Age	Commit message (Expand)	Author
2000-12-14	Les params d'inductif deviennent en même temps propre à chaque inductif d'u...	herbelin
2000-12-14	Amélioration message d'erreur	herbelin
2000-12-14	Raffinement erreur Wrong Predicate	herbelin
2000-12-12	syntaxe AST Inversion + commentaires ocamlweb autour de $	filliatr
2000-12-12	petit bug -byte/-opt (execv -> execvp) et message coercion teste is_silent	filliatr
2000-12-06	Ajout erreur DoesNotOccurIn	herbelin
2000-12-06	Suppresion de l'option -as, c'est maintenant -R qui devient l'option standard...	herbelin
2000-12-06	Reparation conditions de positivites inductifs, echange dans add_entry	mohring
2000-12-05	Mini-nettoyage noms longs	herbelin
2000-12-04	caractere opaque des constantes repris en compte	filliatr
2000-11-30	Changement de la syntaxe des options -I et -R	herbelin
2000-11-29	Bug option -I et -R quand le répertoire est '..'	herbelin
2000-11-29	Bug option -I et -R quand le répertoire est '.'	herbelin
2000-11-29	Suppression cast inutile	herbelin
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_di...	sacerdot
2000-11-29	Ajout d'une option d'alias à -I	herbelin
2000-11-29	Ajout d'un alias à add_path, rec_add_path et all_subdirs pour associer un ch...	herbelin
2000-11-28	Remplacement des add_include par add_rec_include pour avoir le repertoire dan...	herbelin
2000-11-28	Prise en compte du repertoire dans le section path; utilisation de dirpath po...	herbelin
2000-11-27	Distinction local/global	herbelin
2000-11-27	uniformisation messages d'erreur	filliatr
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