aboutsummaryrefslogtreecommitdiff
path: root/library/nametab.ml
AgeCommit message (Expand)Author
2002-05-29Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et co...herbelin
2001-12-13compat ocaml 3.03filliatr
2001-11-19Re-installation de l'affichage des globaux par des noms courtsherbelin
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-11Suppression option immediate_discharge; nettoyage de Declare et conséquencesherbelin
2001-09-20Nettoyage des commentairesherbelin
2001-09-19Ajout de la profondeur de section à DischargeAt pour gérer l'«open» et le...herbelin
2001-09-14Transformation de Remark/Fact en constantes non visibles sans qualificationherbelin
2001-09-07Suppression des library roots, on teste si un nom est absolu autrementherbelin
2001-08-10Parsingherbelin
2001-08-05Ajout error_global_not_foundherbelin
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-02-07Meilleure approche du conflit path/freeze/library_root en séquentialisant la...herbelin
2001-02-07Probleme synchronisation roots / inputstateherbelin
2001-02-07Message d'erreur absolute_referenceherbelin
2001-02-05Meilleur traitement des noms explicites dans la Nametab; Différentation du t...herbelin
2000-12-20Test pour empêcher 2 sections de même nomsherbelin
2000-12-05Nouvelle table de noms pour les locaux qui ne survit pas à la fermeture de l...herbelin
2000-11-29Enregistrement des racines de la bibliothèqueherbelin
2000-11-26Nettoyageherbelin
2000-11-26Prise en compte de noms absolus dans la nametabherbelin
2000-11-24Ajout objets END-SECTION pour les nametabs + nettoyage lib/nametabfilliatr
2000-11-24certains effets disparaissent a la sortie des sections, d'autres non (selon S...filliatr
2000-11-22Abstraction du type 'qualid' pour les noms qualifiés relatifs distinct de 's...herbelin
2000-11-20Nouvelle structure arborescente à la Nametab pour prendre en compte les noms...herbelin
2000-08-21Nametab.init - bug correctedcoq
1999-09-19 - un effort sur la doc (ocamlweb)filliatr