aboutsummaryrefslogtreecommitdiff
path: root/plugins/funind/glob_termops.ml
AgeCommit message (Expand)Author
2010-12-25Rename mkR* smart constructors (mostly in funind)glondu
2010-12-24More {raw => glob} changes for consistencyglondu
2010-12-24Rename files in funind to respect new conventionsglondu