aboutsummaryrefslogtreecommitdiff
path: root/pretyping/glob_term.ml
AgeCommit message (Expand)Author
2011-04-15Take benefit of eta-expansion so that "ex P" is displayed "exists x, P x".herbelin
2010-12-24More {raw => glob} changes for consistencyglondu
2010-12-23Rename rawterm.ml into glob_term.mlglondu