coq - The formal proof system

Age	Commit message (Expand)	Author
2006-05-23	Modification de add_glob (support des modules dans Coqdoc)	notin
2006-01-11	Suppression résidus code v7 et traducteur	herbelin
2005-02-18	Moved Indmap and ConstrMap from Libnames to Names for use in Cooking	herbelin
2004-11-16	Names.substitution (and related functions) and Term.subst_mps moved to	sacerdot
2004-11-16	IMPORTANT COMMIT: constant is now an ADT (it used to be equal to kernel_name).	sacerdot
2004-10-20	COMMITED BYTECODE COMPILER	barras
2004-07-16	Nouvelle en-tête	herbelin
2004-03-28	Désaffectation de l'usage de Top dans Names (maintenant contrôlé dans coqt...	herbelin
2003-03-12	* empty log message *	barras
2003-01-31	* empty log message *	courant
2003-01-22	id_of_msid en plus	letouzey
2002-12-09	Corrections de gestion des univers et modules + meilleure gestions des noms...	coq
2002-12-05	des Set et des Map en plus	letouzey
2002-12-04	Corrige un bug de composition de substitutions	coq
2002-11-14	Réforme de l'interprétation des termes :	herbelin
2002-09-29	Hash-consing pour kernel_name	herbelin
2002-08-19	Pretty-printing preliminaire des modules, commandes	coq
2002-08-02	Modules dans COQ\!\!\!\!	coq
2001-11-29	reparation de Locate	barras
2001-11-29	nouvel algo de conversion plus uniforme	barras
2001-11-05	GROS COMMIT:	barras
2001-10-17	Abstraction de l'immplementation de dirpath et implementation dans l'autre se...	herbelin
2001-10-12	Déplacement de global_reference dans Names pour pouvoir lier Nametab à gra...	herbelin
2001-10-09	Suppression des arguments sur les constantes, inductifs et constructeurs	barras
2001-09-20	Transparent	barras
2001-09-20	Romega	mohring
2001-09-19	Affichage des dir_path vide	herbelin
2001-09-18	Romega/names/Makefile	mohring
2001-09-04	erreur de pretty-print lors de l'affichage de termes avec de Bruijn non lies	barras
2001-08-10	Parsing	herbelin
2001-08-01	Ajout add_prefix/add_suffix	herbelin
2001-03-15	entetes	filliatr
2001-03-01	Déplacement de qualid dans Nametab, hors du noyau	herbelin
2001-02-16	ident au lieu de string pour le nom de base de qualid	herbelin
2001-02-14	Mise en place d'un système optionnel de discharge immédiat; prise en compte...	herbelin
2001-01-31	Ajout d'espace dans les règles d'affichage des infix si des lettres figurent...	herbelin
2001-01-27	Ajout alias mutual_inductive_path = section_path	herbelin
2000-12-25	Alias variable_path	herbelin
2000-12-15	Le bon choix, c'est finalement identifier = string	herbelin
2000-12-15	Mise en place d'un module Ident avec test de l'efficacité quand identifier=s...	herbelin
2000-12-05	Mini-nettoyage noms longs	herbelin
2000-11-29	Ajout d'un test pour vérifier qu'on a affaire à un ident	herbelin
2000-11-28	Prise en compte du repertoire dans le section path; utilisation de dirpath po...	herbelin
2000-11-26	Prise en compte de noms absolus dans la nametab	herbelin
2000-11-23	Affichage des paths avec des '.', print_id -> pr_id, print_sp -> pr_sp	herbelin
2000-11-22	Abstraction du type 'qualid' pour les noms qualifiés relatifs distinct de 's...	herbelin
2000-11-20	Introduction constant_path = section_path	herbelin
2000-11-07	Bug sur précédent commit	herbelin
2000-11-07	Nettoyage Names suite	herbelin
2000-11-06	Nettoyage Names et conséquences (dont ajout d'un type dir_path, argument de ...	herbelin