aboutsummaryrefslogtreecommitdiff
path: root/pretyping/glob_term.mli
AgeCommit message (Expand)Author
2011-01-07mli comments for docpboutill
2010-12-24More {raw => glob} changes for consistencyglondu
2010-12-23Rename rawterm.ml into glob_term.mlglondu