aboutsummaryrefslogtreecommitdiff
path: root/plugins/funind/glob_termops.mli
AgeCommit message (Expand)Author
2015-10-13Fix some typos.Guillaume Melquiond
2012-12-18Modulification of nameppedrot
2012-12-14Modulification of identifierppedrot
2012-06-22Added an indirection with respect to Loc in Compat. As many [open Compat]ppedrot
2012-05-29global_reference migrated from Libnames to new Globnames, less deps in gramma...letouzey
2012-05-29locus.mli for occurrences+clauses, misctypes.mli for various little thingsletouzey
2012-03-02Noise for nothingpboutill
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