aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/names.mli
Commit message (Expand)AuthorAge
* [api] Misctypes removal: miscellaneous aliases.Gravatar Emilio Jesus Gallego Arias2018-06-12
* [api] Remove deprecated aliases from `Names`.Gravatar Emilio Jesus Gallego Arias2018-05-30
* [api] Reintroduce `Names.global_reference` aliasGravatar Emilio Jesus Gallego Arias2018-05-30
* [api] Rename `global_reference` to `GlobRef.t` to follow kernel style.Gravatar Emilio Jesus Gallego Arias2018-05-04
* [api] Deprecate a couple of aliases that we missed.Gravatar Emilio Jesus Gallego Arias2018-03-28
* Allow using cumulativity without forcing strict constraints.Gravatar Gaëtan Gilbert2018-03-09
* Update headers following #6543.Gravatar Théo Zimmermann2018-02-27
* Remove references to removed Unicode.UnsupportedGravatar Jasper Hugunin2018-01-11
* [api] Miscellaneous consolidation + moves to engine.Gravatar Emilio Jesus Gallego Arias2017-11-21
* [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
* deprecate Pp.std_ppcmds type aliasGravatar Matej Košík2017-07-27
* Bump year in headers.Gravatar Pierre-Marie Pédrot2017-07-04
* A few typos.Gravatar Hugo Herbelin2017-06-04
* Creating a module Nameops.Name extending module Names.Name.Gravatar Hugo Herbelin2017-05-31
* Revised behavior on ill-formed identifiers.Gravatar Hugo Herbelin2017-05-20
* [safe_string] library/nameopsGravatar Emilio Jesus Gallego Arias2017-03-14
* COMMENT: Names.Cmap and Names.Cmap_envGravatar Matej Kosik2016-10-26
* Changing the definition of the "Lib.variable.info" type to enable us to do mo...Gravatar Matej Kosik2016-08-24
* Adding a bit of documentation in the mli.Gravatar Pierre-Marie Pédrot2016-06-09
* Checker: avoid using obsolete names from NamesGravatar Pierre Letouzey2016-05-31
* Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-03-30
|\
| * Adding eq/compare/hash for syntactic view atGravatar Hugo Herbelin2016-03-22
| * Hashconsing modules.Gravatar Pierre-Marie Pédrot2016-03-10
* | ADD: Names.Name.is_{anonymous,name}Gravatar Matej Kosik2016-02-18
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-01-21
|\|
| * Update copyright headers.Gravatar Maxime Dénès2016-01-20
* | COMMENTS: added to the "Names.inductive" and "Names.constructor" types.Gravatar Matej Kosik2016-01-11
* | Merge remote-tracking branch 'origin/v8.5' into trunkGravatar Guillaume Melquiond2016-01-06
|\|
| * Protect code against changes in Map interface.Gravatar Maxime Dénès2016-01-06
* | COMMENTS: added to the "Names" module.Gravatar Matej Kosik2015-12-18
* | Hashconsing modules.Gravatar Pierre-Marie Pédrot2015-11-15
* | Better debug printers for module paths.Gravatar Maxime Dénès2015-09-20
| * Reverting 16 last commits, committed mistakenly using the wrong push command.Gravatar Hugo Herbelin2015-08-02
| * Adding eq/compare/hash for syntactic view atGravatar Hugo Herbelin2015-08-02
|/
* Display functions for primitive projections.Gravatar Maxime Dénès2015-07-02
* Fixing bug #4190.Gravatar Pierre-Marie Pédrot2015-04-16
* Correct restriction of vm_compute when handling universe polymorphicGravatar Matthieu Sozeau2015-01-15
* Update headers.Gravatar Maxime Dénès2015-01-12
* Fix (actually, properly implement :) hashconsing of projections,Gravatar Matthieu Sozeau2014-12-17
* Add a boolean to indicate the unfolding state of a primitive projection,Gravatar Matthieu Sozeau2014-09-27
* 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
* Also use HMaps in KNmap.Gravatar Pierre-Marie Pédrot2014-03-08
* Using Hashmaps by default in constant and inductive maps. This changes fold andGravatar Pierre-Marie Pédrot2014-03-07
* Inductive maps in Environ now use HMap.Gravatar Pierre-Marie Pédrot2014-03-06
* Lazily computed hash in KerName.t.Gravatar Pierre-Marie Pédrot2014-03-05
* Fixing generic hashes and replacing them with proper ones.Gravatar Pierre-Marie Pédrot2014-03-03