aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/syntax_def.ml
Commit message (Expand)AuthorAge
* Cablage des syntactif defs avec la Nametab des objetsGravatar herbelin2000-11-20
* methode exportGravatar filliatr2000-11-15
* Bugs lies a la confusion load/open et a un open abusivement recursif dans lib...Gravatar herbelin2000-11-10
* Syntactic Definition n'etaient pas correctemenet importeesGravatar filliatr2000-03-16
* changement type add_anonymous_leafGravatar filliatr1999-12-05
* modifs pour premiere edition de liensGravatar filliatr1999-12-02