aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/funind/indfun.mli
Commit message (Expand)AuthorAge
* Rename rawterm.ml into glob_term.mlGravatar glondu2010-12-23
* Using vernac parsing for FunctionGravatar jforest2010-06-08