aboutsummaryrefslogtreecommitdiffhomepage
path: root/library/globnames.mli
Commit message (Expand)AuthorAge
* Update copyright headers.Gravatar Maxime Dénès2016-01-20
* Update headers.Gravatar Maxime Dénès2015-01-12
* This commit adds full universe polymorphism and fast projections to Coq.Gravatar Matthieu Sozeau2014-05-06
* Removing dead code, thanks to new OCaml warnings and a bit of scripting.Gravatar Pierre-Marie Pédrot2014-04-23
* Missing equalities in Names-like structures.Gravatar Pierre-Marie Pédrot2014-03-20
* Using HMaps in global references.Gravatar Pierre-Marie Pédrot2014-03-08
* Remove many superfluous 'open' indicated by ocamlc -w +33Gravatar Pierre Letouzey2014-03-05
* Added a more efficient way to recover the domain of a map.Gravatar ppedrot2013-08-25
* Dir_path --> DirPathGravatar letouzey2013-02-19
* Classops : avoid some use of GmapGravatar letouzey2013-02-19
* Modulification of dir_pathGravatar ppedrot2012-12-14
* Modulification of identifierGravatar ppedrot2012-12-14
* Finish patch for Hint Resolve, stopping to generate new constant names forGravatar msozeau2012-12-08
* 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-30 00:09:09 +0000