aboutsummaryrefslogtreecommitdiffhomepage
path: root/library/nametab.ml
Commit message (Expand)AuthorAge
* Nouvelle table de noms pour les locaux qui ne survit pas à la fermeture de l...Gravatar herbelin2000-12-05
* Enregistrement des racines de la bibliothèqueGravatar herbelin2000-11-29
* NettoyageGravatar herbelin2000-11-26
* Prise en compte de noms absolus dans la nametabGravatar herbelin2000-11-26
* Ajout objets END-SECTION pour les nametabs + nettoyage lib/nametabGravatar filliatr2000-11-24
* certains effets disparaissent a la sortie des sections, d'autres non (selon S...Gravatar filliatr2000-11-24
* Abstraction du type 'qualid' pour les noms qualifiés relatifs distinct de 's...Gravatar herbelin2000-11-22
* Nouvelle structure arborescente à la Nametab pour prendre en compte les noms...Gravatar herbelin2000-11-20
* Nametab.init - bug correctedGravatar coq2000-08-21
* - un effort sur la doc (ocamlweb)Gravatar filliatr1999-09-19