aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/funind/glob_termops.mli
Commit message (Expand)AuthorAge
* [API] Remove `open API` in ml files in favor of `-open API` flag.Gravatar Emilio Jesus Gallego Arias2017-07-17
* Put all plugins behind an "API".Gravatar Matej Kosik2017-06-07
* solving implicit resolution in FunctionGravatar Julien Forest2017-06-01
* [location] Switch glob_constr to Loc.locatedGravatar Emilio Jesus Gallego Arias2017-04-24
* Replacing "cast surgery" in LetIn by a proper field (see PR #404).Gravatar Hugo Herbelin2017-03-24
* 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-22 21:54:48 +0000