aboutsummaryrefslogtreecommitdiff
path: root/library/nametab.mli
AgeCommit message (Expand)Author
2000-11-21implicites manuelsfilliatr
2000-11-20Nouvelle structure arborescente à la Nametab pour prendre en compte les noms...herbelin
1999-09-28juste l'interface de Dischargefilliatr
1999-09-19 - un effort sur la doc (ocamlweb)filliatr