aboutsummaryrefslogtreecommitdiffhomepage
path: root/library/globnames.ml
Commit message (Expand)AuthorAge
* [api] Remove deprecated objects in engine / interp / libraryGravatar Emilio Jesus Gallego Arias2018-05-30
* [api] Rename `global_reference` to `GlobRef.t` to follow kernel style.Gravatar Emilio Jesus Gallego Arias2018-05-04
* Allow using cumulativity without forcing strict constraints.Gravatar Gaëtan Gilbert2018-03-09
* Update headers following #6543.Gravatar Théo Zimmermann2018-02-27
* Use r.(p) syntax to print primitive projections.Gravatar Maxime Dénès2018-01-30
* [api] Move structures deprecated in the API to the core.Gravatar Emilio Jesus Gallego Arias2017-11-06
* [api] Deprecate all legacy uses of Names in core.Gravatar Emilio Jesus Gallego Arias2017-11-06
* [api] Deprecate all legacy uses of Name.Id in core.Gravatar Emilio Jesus Gallego Arias2017-11-04
* Bump year in headers.Gravatar Pierre-Marie Pédrot2017-07-04
* Drop '.' from CErrors.anomaly, insert it in argsGravatar Jason Gross2017-06-02
* errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...Gravatar Pierre Letouzey2016-07-03
* Merge branch 'linear-comparison' of https://github.com/aspiwack/coq into aspi...Gravatar Matthieu Sozeau2016-04-04
|\
* \ Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-01-21
|\ \
| * | Update copyright headers.Gravatar Maxime Dénès2016-01-20
* | | COMMENTS: added to some variants of "Globalnames.global_reference" type.Gravatar Matej Kosik2015-12-18
|/ /
| * More uniformity in the style of comparison functions.Gravatar Arnaud Spiwack2015-10-30
| * Make the code of compare functions linear in the number of constructors.Gravatar Arnaud Spiwack2015-10-29
|/
* Removing dead code.Gravatar Pierre-Marie Pédrot2015-02-02
* 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
* 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
* Fixing pervasive comparisonsGravatar Pierre-Marie Pédrot2014-03-01
* Partial application in Globnames.Gravatar ppedrot2013-11-06
* Removing some generic equalities.Gravatar ppedrot2013-10-22
* Added a more efficient way to recover the domain of a map.Gravatar ppedrot2013-08-25
* Names: shortcuts for building {kn, constant, mind} with empty sectionsGravatar letouzey2013-02-26
* Dir_path --> DirPathGravatar letouzey2013-02-19
* Classops : avoid some use of GmapGravatar letouzey2013-02-19
* Names: revised representation of constants and mutual_inductiveGravatar letouzey2013-02-19
* Minor code cleanups, especially take advantage of Dir_path.is_emptyGravatar letouzey2013-02-18
* Uniformization of the "anomaly" command.Gravatar ppedrot2013-01-28
* Modulification of mod_bound_idGravatar ppedrot2012-12-18
* Modulification of LabelGravatar ppedrot2012-12-18
* 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
* Monomorphization (library)Gravatar ppedrot2012-11-22
* Remove some more "open" and dead code thanks to OCaml4 warningsGravatar letouzey2012-10-02
* Partial revert of Yann commit in order to use CLib.List when openingGravatar ppedrot2012-09-14
* This patch removes unused "open" (automatically generated fromGravatar regisgia2012-09-14
* Updating headers.Gravatar herbelin2012-08-08
* global_reference migrated from Libnames to new Globnames, less deps in gramma...Gravatar letouzey2012-05-29