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