aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/funind/glob_termops.ml
Commit message (Expand)AuthorAge
* Rename mkR* smart constructors (mostly in funind)Gravatar glondu2010-12-25
* More {raw => glob} changes for consistencyGravatar glondu2010-12-24
* Rename files in funind to respect new conventionsGravatar glondu2010-12-24