coq - The formal proof system

Age	Commit message (Expand)	Author
2008-07-15	Autour du parsing:	herbelin
2008-06-25	Création du fichier dumpglob.ml, qui rassemble les fonctions de globalisatio...	notin
2008-05-11	- Cleanup parsing of binders, reducing to a single production for all	msozeau
2008-04-23	Prise en compte des coercions dans les clauses "with" même si le type	herbelin
2008-04-21	- Parameterize unification by two sets of transparent_state, one for open	msozeau
2008-04-14	suite 10790 (identificateurs)	herbelin
2008-04-13	Bugs, nettoyage, et améliorations diverses	herbelin
2007-12-18	Nettoyage de code en vue de la release. Plus de Warning: Unused	aspiwack
2007-05-11	Processor integers + Print assumption (see coqdev mailing list for the	aspiwack
2007-02-21	Fixed the pseudo-cicularity problem due to the with operator on Module Type.	soubiran
2007-01-24	modifications des messages d'erreurs renvoyés lors de la comparaison	soubiran
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