aboutsummaryrefslogtreecommitdiff
path: root/kernel/names.mli
AgeCommit message (Expand)Author
2018-06-12[api] Misctypes removal: miscellaneous aliases.Emilio Jesus Gallego Arias
2018-05-30[api] Remove deprecated aliases from `Names`.Emilio Jesus Gallego Arias
2018-05-30[api] Reintroduce `Names.global_reference` aliasEmilio Jesus Gallego Arias
2018-05-04[api] Rename `global_reference` to `GlobRef.t` to follow kernel style.Emilio Jesus Gallego Arias
2018-03-28[api] Deprecate a couple of aliases that we missed.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-11Remove references to removed Unicode.UnsupportedJasper Hugunin
2017-11-21[api] Miscellaneous consolidation + moves to engine.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-11-04[api] Deprecate all legacy uses of Name.Id in core.Emilio Jesus Gallego Arias
2017-07-27deprecate Pp.std_ppcmds type aliasMatej Košík
2017-07-04Bump year in headers.Pierre-Marie Pédrot
2017-06-04A few typos.Hugo Herbelin
2017-05-31Creating a module Nameops.Name extending module Names.Name.Hugo Herbelin
2017-05-20Revised behavior on ill-formed identifiers.Hugo Herbelin
2017-03-14[safe_string] library/nameopsEmilio Jesus Gallego Arias
2016-10-26COMMENT: Names.Cmap and Names.Cmap_envMatej Kosik
2016-08-24Changing the definition of the "Lib.variable.info" type to enable us to do mo...Matej Kosik
2016-06-09Adding a bit of documentation in the mli.Pierre-Marie Pédrot
2016-05-31Checker: avoid using obsolete names from NamesPierre Letouzey
2016-03-30Merge branch 'v8.5'Pierre-Marie Pédrot
2016-03-22Adding eq/compare/hash for syntactic view atHugo Herbelin
2016-03-10Hashconsing modules.Pierre-Marie Pédrot
2016-02-18ADD: Names.Name.is_{anonymous,name}Matej Kosik
2016-01-21Merge branch 'v8.5'Pierre-Marie Pédrot
2016-01-20Update copyright headers.Maxime Dénès
2016-01-11COMMENTS: added to the "Names.inductive" and "Names.constructor" types.Matej Kosik
2016-01-06Merge remote-tracking branch 'origin/v8.5' into trunkGuillaume Melquiond
2016-01-06Protect code against changes in Map interface.Maxime Dénès
2015-12-18COMMENTS: added to the "Names" module.Matej Kosik
2015-11-15Hashconsing modules.Pierre-Marie Pédrot
2015-09-20Better debug printers for module paths.Maxime Dénès
2015-08-02Reverting 16 last commits, committed mistakenly using the wrong push command.Hugo Herbelin
2015-08-02Adding eq/compare/hash for syntactic view atHugo Herbelin
2015-07-02Display functions for primitive projections.Maxime Dénès
2015-04-16Fixing bug #4190.Pierre-Marie Pédrot
2015-01-15Correct restriction of vm_compute when handling universe polymorphicMatthieu Sozeau
2015-01-12Update headers.Maxime Dénès
2014-12-17Fix (actually, properly implement :) hashconsing of projections,Matthieu Sozeau
2014-09-27Add a boolean to indicate the unfolding state of a primitive projection,Matthieu Sozeau
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-08Also use HMaps in KNmap.Pierre-Marie Pédrot
2014-03-07Using Hashmaps by default in constant and inductive maps. This changes fold andPierre-Marie Pédrot
2014-03-06Inductive maps in Environ now use HMap.Pierre-Marie Pédrot
2014-03-05Lazily computed hash in KerName.t.Pierre-Marie Pédrot
2014-03-03Fixing generic hashes and replacing them with proper ones.Pierre-Marie Pédrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 22:01:58 +0000