aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/funind/glob_termops.mli
Commit message (Expand)AuthorAge
* Fix some typos.Gravatar Guillaume Melquiond2015-10-13
* Modulification of nameGravatar ppedrot2012-12-18
* Modulification of identifierGravatar ppedrot2012-12-14
* Added an indirection with respect to Loc in Compat. As many [open Compat]Gravatar ppedrot2012-06-22
* global_reference migrated from Libnames to new Globnames, less deps in gramma...Gravatar letouzey2012-05-29
* locus.mli for occurrences+clauses, misctypes.mli for various little thingsGravatar letouzey2012-05-29
* Noise for nothingGravatar pboutill2012-03-02
* 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