aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/names.mli
Commit message (Expand)AuthorAge
* 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
* 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
* 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
* Suites modifs du noyau. Univ devient purement fonctionnel.Gravatar barras2001-11-12
* 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
* Compatibilté make docGravatar herbelin2001-09-20
* 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 alias mutual_inductive_path = section_pathGravatar herbelin2001-01-27
* Alias variable_pathGravatar herbelin2000-12-25
* syntaxe AST Inversion + commentaires ocamlweb autour de $Gravatar filliatr2000-12-12
* Mini-nettoyage noms longsGravatar herbelin2000-12-05
* Ajout d'un test pour vérifier qu'on a affaire à un identGravatar herbelin2000-11-29
* Prise en compte de noms absolus dans la nametabGravatar herbelin2000-11-26
* Affichage des paths avec des '.', print_id -> pr_id, print_sp -> pr_spGravatar herbelin2000-11-23
* Abstraction du type 'qualid' pour les noms qualifiés relatifs distinct de 's...Gravatar herbelin2000-11-22
* implicites manuelsGravatar filliatr2000-11-21
* Introduction constant_path = section_pathGravatar herbelin2000-11-20
* Nettoyage Names suiteGravatar herbelin2000-11-07
* Nettoyage Names et conséquences (dont ajout d'un type dir_path, argument de ...Gravatar herbelin2000-11-06
* Passage à des contextes de vars et de rels pouvant contenir des déclarationsGravatar herbelin2000-07-24
* modifs pour premiere edition de liensGravatar filliatr1999-12-02
* Intégration du Termast et du Retyping de HH, et modifications connexesGravatar herbelin1999-12-01
* diverses fonctions ajouteesGravatar filliatr1999-12-01
* - un effort sur la doc (ocamlweb)Gravatar filliatr1999-09-19
* modules System, Lib et StatesGravatar filliatr1999-09-10
* - environnements videsGravatar filliatr1999-09-03
* un petit effort de presentation dans les interfacesGravatar filliatr1999-08-30
* mise en place programmation literaire (generation de doc/coq.tex)Gravatar filliatr1999-08-19
* module Reduction (debut)Gravatar filliatr1999-08-18
* generic, term et evdGravatar filliatr1999-08-17
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-25 17:09:57 +0000