aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/names.ml
Commit message (Expand)AuthorAge
* - coq_makefile: target install now respects the original tree structureGravatar herbelin2008-12-24
* Report des commits 11417 et 11437 de la v8.2Gravatar soubiran2008-10-15
* Autour du parsing:Gravatar herbelin2008-07-15
* Création du fichier dumpglob.ml, qui rassemble les fonctions de globalisatio...Gravatar notin2008-06-25
* - Cleanup parsing of binders, reducing to a single production for allGravatar msozeau2008-05-11
* Prise en compte des coercions dans les clauses "with" même si le typeGravatar herbelin2008-04-23
* - Parameterize unification by two sets of transparent_state, one for openGravatar msozeau2008-04-21
* suite 10790 (identificateurs)Gravatar herbelin2008-04-14
* Bugs, nettoyage, et améliorations diversesGravatar herbelin2008-04-13
* Nettoyage de code en vue de la release. Plus de Warning: Unused Gravatar aspiwack2007-12-18
* Processor integers + Print assumption (see coqdev mailing list for the Gravatar aspiwack2007-05-11
* Fixed the pseudo-cicularity problem due to the with operator on Module Type.Gravatar soubiran2007-02-21
* modifications des messages d'erreurs renvoyés lors de la comparaison Gravatar soubiran2007-01-24
* Modification de add_glob (support des modules dans Coqdoc)Gravatar notin2006-05-23
* Suppression résidus code v7 et traducteurGravatar herbelin2006-01-11
* Moved Indmap and ConstrMap from Libnames to Names for use in CookingGravatar herbelin2005-02-18
* Names.substitution (and related functions) and Term.subst_mps moved toGravatar sacerdot2004-11-16
* IMPORTANT COMMIT: constant is now an ADT (it used to be equal to kernel_name).Gravatar sacerdot2004-11-16
* COMMITED BYTECODE COMPILERGravatar barras2004-10-20
* Nouvelle en-têteGravatar herbelin2004-07-16
* Désaffectation de l'usage de Top dans Names (maintenant contrôlé dans coqt...Gravatar herbelin2004-03-28
* *** empty log message ***Gravatar barras2003-03-12
* *** empty log message ***Gravatar courant2003-01-31
* id_of_msid en plusGravatar letouzey2003-01-22
* Corrections de gestion des univers et modules + meilleure gestions des noms...Gravatar coq2002-12-09
* des Set et des Map en plusGravatar letouzey2002-12-05
* Corrige un bug de composition de substitutionsGravatar coq2002-12-04
* Réforme de l'interprétation des termes :Gravatar herbelin2002-11-14
* Hash-consing pour kernel_nameGravatar herbelin2002-09-29
* Pretty-printing preliminaire des modules, commandesGravatar coq2002-08-19
* Modules dans COQ\!\!\!\!Gravatar coq2002-08-02
* reparation de LocateGravatar barras2001-11-29
* nouvel algo de conversion plus uniformeGravatar barras2001-11-29
* GROS COMMIT:Gravatar barras2001-11-05
* Abstraction de l'immplementation de dirpath et implementation dans l'autre se...Gravatar herbelin2001-10-17
* Déplacement de global_reference dans Names pour pouvoir lier Nametab à gra...Gravatar herbelin2001-10-12
* Suppression des arguments sur les constantes, inductifs et constructeursGravatar barras2001-10-09
* TransparentGravatar barras2001-09-20
* RomegaGravatar mohring2001-09-20
* Affichage des dir_path videGravatar herbelin2001-09-19
* Romega/names/MakefileGravatar mohring2001-09-18
* erreur de pretty-print lors de l'affichage de termes avec de Bruijn non liesGravatar barras2001-09-04
* ParsingGravatar herbelin2001-08-10
* Ajout add_prefix/add_suffixGravatar herbelin2001-08-01
* entetesGravatar filliatr2001-03-15
* Déplacement de qualid dans Nametab, hors du noyauGravatar herbelin2001-03-01
* ident au lieu de string pour le nom de base de qualidGravatar herbelin2001-02-16
* Mise en place d'un système optionnel de discharge immédiat; prise en compte...Gravatar herbelin2001-02-14
* Ajout d'espace dans les règles d'affichage des infix si des lettres figurent...Gravatar herbelin2001-01-31
* Ajout alias mutual_inductive_path = section_pathGravatar herbelin2001-01-27