coq - The formal proof system

Age	Commit message (Expand)	Author
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
2000-10-23	L'état implicite des définitions survivant au discharge redevient celui du ...	herbelin
2000-10-18	Simplifications autour de typed_type (renommé types par analogie avec sorts)...	herbelin
2000-10-18	Renommage canonique :	herbelin
2000-10-16	Correction bug affichage des infix	herbelin
2000-10-13	Suppression du test de convertibilite inutile pour la plupart des exact; 2 ve...	herbelin
2000-10-12	Hypotheses des ind oubliees dans le discharge	herbelin
2000-10-11	Message d'erreur bad pattern	herbelin
2000-10-10	Messages d'erreurs Cases	herbelin
2000-10-06	Correction incompatibilites dans la fn des types des inductifs	herbelin
2000-10-01	Renommage AppL en App	herbelin
2000-10-01	renommage map_constr_with_named_binders	herbelin
2000-10-01	Disparition du type oper mais nouveau type global_reference	herbelin
2000-10-01	Code mort	herbelin
2000-09-15	Messages d'erreurs	herbelin