aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/funind/invfun.mli
Commit message (Expand)AuthorAge
* [api] Misctypes removal: several moves:Gravatar Emilio Jesus Gallego Arias2018-06-12
* [api] Rename `global_reference` to `GlobRef.t` to follow kernel style.Gravatar Emilio Jesus Gallego Arias2018-05-04
* Update headers following #6543.Gravatar Théo Zimmermann2018-02-27
* Remove dead code from funind.Gravatar Maxime Dénès2018-01-24