aboutsummaryrefslogtreecommitdiff
path: root/pretyping/glob_term.ml
AgeCommit message (Expand)Author
2012-03-02Glob_term.predicate_pattern: No number of parameters with letins.pboutill
2012-03-02Noise for nothingpboutill
2012-01-30Added an pattern / occurence syntax for vm_compute.ppedrot
2011-10-28Remove dynamic stuff from constr_expr and glob_constrglondu
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