aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/glob_term.mli
Commit message (Expand)AuthorAge
* mli comments for docGravatar pboutill2011-01-07
* More {raw => glob} changes for consistencyGravatar glondu2010-12-24
* Rename rawterm.ml into glob_term.mlGravatar glondu2010-12-23