aboutsummaryrefslogtreecommitdiff
path: root/plugins/funind/invfun.mli
AgeCommit message (Expand)Author
2018-06-12[api] Misctypes removal: several moves:Emilio Jesus Gallego Arias
2018-05-04[api] Rename `global_reference` to `GlobRef.t` to follow kernel style.Emilio Jesus Gallego Arias
2018-02-27Update headers following #6543.Théo Zimmermann
2018-01-24Remove dead code from funind.Maxime Dénès