aboutsummaryrefslogtreecommitdiff
path: root/library/globnames.ml
AgeCommit message (Expand)Author
2021-03-26[recordops] complete API rewrite; the module is now called [structures]Enrico Tassi
2020-10-21Rename the GlobRef comparison modules following the standard pattern.Pierre-Marie Pédrot
2020-04-13pass filters aroundGaëtan Gilbert
2020-04-13Add ExtRefMap/Set to globnamesGaëtan Gilbert
2020-03-18Update headers in the whole code base.Théo Zimmermann
2020-02-12Standardize constr -> globref operations to use destRef/isRef/isRefXGaëtan Gilbert
2020-01-28Remove dead code in Globnames.Pierre-Marie Pédrot
2019-07-08[api] Deprecate GlobRef constructors.Emilio Jesus Gallego Arias
2019-06-17Update ml-style headers to new year.Théo Zimmermann
2019-05-10[api] Remove 8.10 deprecations.Emilio Jesus Gallego Arias
2018-12-05Fix mod_subst wrt universe polymorphismGaëtan Gilbert
2018-10-05[kernel] Remove section paths from `KerName.t`Maxime Dénès
2018-09-12Move maps & sets indexed by GlobRef.t into the kernelVincent Laporte
2018-05-30[api] Remove deprecated objects in engine / interp / libraryEmilio Jesus Gallego Arias
2018-05-04[api] Rename `global_reference` to `GlobRef.t` to follow kernel style.Emilio Jesus Gallego Arias
2018-03-09Allow using cumulativity without forcing strict constraints.Gaëtan Gilbert
2018-02-27Update headers following #6543.Théo Zimmermann
2018-01-30Use r.(p) syntax to print primitive projections.Maxime Dénès
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-11-04[api] Deprecate all legacy uses of Name.Id in core.Emilio Jesus Gallego Arias
2017-07-04Bump year in headers.Pierre-Marie Pédrot
2017-06-02Drop '.' from CErrors.anomaly, insert it in argsJason Gross
2016-07-03errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...Pierre Letouzey
2016-04-04Merge branch 'linear-comparison' of https://github.com/aspiwack/coq into aspi...Matthieu Sozeau
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-10-30More uniformity in the style of comparison functions.Arnaud Spiwack
2015-10-29Make the code of compare functions linear in the number of constructors.Arnaud Spiwack
2015-02-02Removing dead code.Pierre-Marie Pédrot
2015-01-12Update headers.Maxime Dénès
2014-05-06This commit adds full universe polymorphism and fast projections to Coq.Matthieu Sozeau
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-01Fixing pervasive comparisonsPierre-Marie Pédrot
2013-11-06Partial application in Globnames.ppedrot
2013-10-22Removing some generic equalities.ppedrot
2013-08-25Added a more efficient way to recover the domain of a map.ppedrot
2013-02-26Names: shortcuts for building {kn, constant, mind} with empty sectionsletouzey
2013-02-19Dir_path --> DirPathletouzey
2013-02-19Classops : avoid some use of Gmapletouzey
2013-02-19Names: revised representation of constants and mutual_inductiveletouzey
2013-02-18Minor code cleanups, especially take advantage of Dir_path.is_emptyletouzey
2013-01-28Uniformization of the "anomaly" command.ppedrot
2012-12-18Modulification of mod_bound_idppedrot
2012-12-18Modulification of Labelppedrot
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 13:05:57 +0000