aboutsummaryrefslogtreecommitdiff
path: root/kernel/names.mli
AgeCommit message (Expand)Author
2009-10-21This big commit addresses two problems:soubiran
2009-09-17Delete trailing whitespaces in all *.{v,ml*} filesglondu
2008-10-15Report des commits 11417 et 11437 de la v8.2soubiran
2008-06-25Cré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 allmsozeau
2008-04-21- Parameterize unification by two sets of transparent_state, one for openmsozeau
2007-12-18Nettoyage de code en vue de la release. Plus de Warning: Unused aspiwack
2007-05-11Processor integers + Print assumption (see coqdev mailing list for the aspiwack
2007-02-21Fixed the pseudo-cicularity problem due to the with operator on Module Type.soubiran
2007-01-24modifications des messages d'erreurs renvoyés lors de la comparaison soubiran
2006-05-23Modification de add_glob (support des modules dans Coqdoc)notin
2005-02-18Moved Indmap and ConstrMap from Libnames to Names for use in Cookingherbelin
2004-11-16Names.substitution (and related functions) and Term.subst_mps moved tosacerdot
2004-11-16IMPORTANT COMMIT: constant is now an ADT (it used to be equal to kernel_name).sacerdot
2004-10-20COMMITED BYTECODE COMPILERbarras
2004-07-16Nouvelle en-têteherbelin
2003-01-22id_of_msid en plusletouzey
2002-12-09Corrections de gestion des univers et modules + meilleure gestions des noms...coq
2002-12-05des Set et des Map en plusletouzey
2002-12-04Corrige un bug de composition de substitutionscoq
2002-11-14Réforme de l'interprétation des termes :herbelin
2002-08-19Pretty-printing preliminaire des modules, commandescoq
2002-08-02Modules dans COQ\!\!\!\!coq
2001-11-29reparation de Locatebarras
2001-11-29nouvel algo de conversion plus uniformebarras
2001-11-12Suites modifs du noyau. Univ devient purement fonctionnel.barras
2001-11-05GROS COMMIT:barras
2001-10-17Abstraction de l'immplementation de dirpath et implementation dans l'autre se...herbelin
2001-10-12Déplacement de global_reference dans Names pour pouvoir lier Nametab à gra...herbelin
2001-10-09Suppression des arguments sur les constantes, inductifs et constructeursbarras
2001-09-20Transparentbarras
2001-09-20Compatibilté make docherbelin
2001-08-10Parsingherbelin
2001-08-01Ajout add_prefix/add_suffixherbelin
2001-03-15entetesfilliatr
2001-03-01Déplacement de qualid dans Nametab, hors du noyauherbelin
2001-02-16ident au lieu de string pour le nom de base de qualidherbelin
2001-02-14Mise en place d'un système optionnel de discharge immédiat; prise en compte...herbelin
2001-01-27Ajout alias mutual_inductive_path = section_pathherbelin
2000-12-25Alias variable_pathherbelin
2000-12-12syntaxe AST Inversion + commentaires ocamlweb autour de $filliatr
2000-12-05Mini-nettoyage noms longsherbelin
2000-11-29Ajout d'un test pour vérifier qu'on a affaire à un identherbelin
2000-11-26Prise en compte de noms absolus dans la nametabherbelin
2000-11-23Affichage des paths avec des '.', print_id -> pr_id, print_sp -> pr_spherbelin
2000-11-22Abstraction du type 'qualid' pour les noms qualifiés relatifs distinct de 's...herbelin
2000-11-21implicites manuelsfilliatr
2000-11-20Introduction constant_path = section_pathherbelin
2000-11-07Nettoyage Names suiteherbelin
2000-11-06Nettoyage Names et conséquences (dont ajout d'un type dir_path, argument de ...herbelin