aboutsummaryrefslogtreecommitdiffhomepage
path: root/library/globnames.mli
Commit message (Expand)AuthorAge
* Updating headers.Gravatar herbelin2012-08-08
* remove many excessive open Util & Errors in mli'sGravatar letouzey2012-05-29
* global_reference migrated from Libnames to new Globnames, less deps in gramma...Gravatar letouzey2012-05-29