aboutsummaryrefslogtreecommitdiff
path: root/library/globnames.mli
AgeCommit message (Expand)Author
2013-02-19Dir_path --> DirPathletouzey
2013-02-19Classops : avoid some use of Gmapletouzey
2012-12-14Modulification of dir_pathppedrot
2012-12-14Modulification of identifierppedrot
2012-12-08Finish patch for Hint Resolve, stopping to generate new constant names formsozeau
2012-08-08Updating headers.herbelin
2012-05-29remove many excessive open Util & Errors in mli'sletouzey
2012-05-29global_reference migrated from Libnames to new Globnames, less deps in gramma...letouzey