coq - The formal proof system

Age	Commit message (Expand)	Author
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
2000-09-15	Expression anglaise	herbelin
2000-09-14	Abstraction de constr	herbelin
2000-09-12	Modification mkAppL; abstraction via kind_of_term; changement dans Reduction	herbelin
2000-09-10	Correction pour make doc	herbelin
2000-09-10	Suppression de Abst	herbelin
2000-09-10	Ajout d'un LetIn primitif.	herbelin
2000-09-10	Uniformisation AddPath, Print LoadPath, ... en Add Path, Print Path. Abstract...	herbelin
2000-09-06	Canonisation de certains noms dans Pretyping, Asterm et Safe_typing	herbelin
2000-09-06	kernel/type_errors.ml	herbelin
2000-07-25	retablissement make doc et make minicoq	filliatr
2000-07-24	Passage à des contextes de vars et de rels pouvant contenir des déclarations	herbelin
2000-07-21	retablissement minicoq (pour Jacek)	filliatr
2000-07-21	Fail n + appel de interp	delahaye
2000-07-01	Précalcul de la forme canonique des constructeurs et arités pour traiter le...	herbelin