aboutsummaryrefslogtreecommitdiff
path: root/library/globnames.mli
AgeCommit message (Expand)Author
2017-11-13[api] Insert miscellaneous API deprecation back to core.Emilio Jesus Gallego Arias
2017-11-06[api] Move structures deprecated in the API to the core.Emilio Jesus Gallego Arias
2017-11-06[api] Deprecate all legacy uses of Names in core.Emilio Jesus Gallego Arias
2017-07-04Bump year in headers.Pierre-Marie Pédrot
2016-01-21Merge branch 'v8.5'Pierre-Marie Pédrot
2016-01-20Update copyright headers.Maxime Dénès
2015-12-18COMMENTS: added to some variants of "Globalnames.global_reference" type.Matej Kosik
2015-01-12Update headers.Maxime Dénès
2014-05-06This commit adds full universe polymorphism and fast projections to Coq.Matthieu Sozeau
2014-04-23Removing dead code, thanks to new OCaml warnings and a bit of scripting.Pierre-Marie Pédrot
2014-03-20Missing equalities in Names-like structures.Pierre-Marie Pédrot
2014-03-08Using HMaps in global references.Pierre-Marie Pédrot
2014-03-05Remove many superfluous 'open' indicated by ocamlc -w +33Pierre Letouzey
2013-08-25Added a more efficient way to recover the domain of a map.ppedrot
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