index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
kernel
/
names.mli
Commit message (
Expand
)
Author
Age
*
[api] Misctypes removal: miscellaneous aliases.
Emilio Jesus Gallego Arias
2018-06-12
*
[api] Remove deprecated aliases from `Names`.
Emilio Jesus Gallego Arias
2018-05-30
*
[api] Reintroduce `Names.global_reference` alias
Emilio Jesus Gallego Arias
2018-05-30
*
[api] Rename `global_reference` to `GlobRef.t` to follow kernel style.
Emilio Jesus Gallego Arias
2018-05-04
*
[api] Deprecate a couple of aliases that we missed.
Emilio Jesus Gallego Arias
2018-03-28
*
Allow using cumulativity without forcing strict constraints.
Gaëtan Gilbert
2018-03-09
*
Update headers following #6543.
Théo Zimmermann
2018-02-27
*
Remove references to removed Unicode.Unsupported
Jasper Hugunin
2018-01-11
*
[api] Miscellaneous consolidation + moves to engine.
Emilio Jesus Gallego Arias
2017-11-21
*
[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-06
*
[api] Deprecate all legacy uses of Name.Id in core.
Emilio Jesus Gallego Arias
2017-11-04
*
deprecate Pp.std_ppcmds type alias
Matej Košík
2017-07-27
*
Bump year in headers.
Pierre-Marie Pédrot
2017-07-04
*
A few typos.
Hugo Herbelin
2017-06-04
*
Creating a module Nameops.Name extending module Names.Name.
Hugo Herbelin
2017-05-31
*
Revised behavior on ill-formed identifiers.
Hugo Herbelin
2017-05-20
*
[safe_string] library/nameops
Emilio Jesus Gallego Arias
2017-03-14
*
COMMENT: Names.Cmap and Names.Cmap_env
Matej Kosik
2016-10-26
*
Changing the definition of the "Lib.variable.info" type to enable us to do mo...
Matej Kosik
2016-08-24
*
Adding a bit of documentation in the mli.
Pierre-Marie Pédrot
2016-06-09
*
Checker: avoid using obsolete names from Names
Pierre Letouzey
2016-05-31
*
Merge branch 'v8.5'
Pierre-Marie Pédrot
2016-03-30
|
\
|
*
Adding eq/compare/hash for syntactic view at
Hugo Herbelin
2016-03-22
|
*
Hashconsing modules.
Pierre-Marie Pédrot
2016-03-10
*
|
ADD: Names.Name.is_{anonymous,name}
Matej Kosik
2016-02-18
*
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2016-01-21
|
\
|
|
*
Update copyright headers.
Maxime Dénès
2016-01-20
*
|
COMMENTS: added to the "Names.inductive" and "Names.constructor" types.
Matej Kosik
2016-01-11
*
|
Merge remote-tracking branch 'origin/v8.5' into trunk
Guillaume Melquiond
2016-01-06
|
\
|
|
*
Protect code against changes in Map interface.
Maxime Dénès
2016-01-06
*
|
COMMENTS: added to the "Names" module.
Matej Kosik
2015-12-18
*
|
Hashconsing modules.
Pierre-Marie Pédrot
2015-11-15
*
|
Better debug printers for module paths.
Maxime Dénès
2015-09-20
|
*
Reverting 16 last commits, committed mistakenly using the wrong push command.
Hugo Herbelin
2015-08-02
|
*
Adding eq/compare/hash for syntactic view at
Hugo Herbelin
2015-08-02
|
/
*
Display functions for primitive projections.
Maxime Dénès
2015-07-02
*
Fixing bug #4190.
Pierre-Marie Pédrot
2015-04-16
*
Correct restriction of vm_compute when handling universe polymorphic
Matthieu Sozeau
2015-01-15
*
Update headers.
Maxime Dénès
2015-01-12
*
Fix (actually, properly implement :) hashconsing of projections,
Matthieu Sozeau
2014-12-17
*
Add a boolean to indicate the unfolding state of a primitive projection,
Matthieu Sozeau
2014-09-27
*
This commit adds full universe polymorphism and fast projections to Coq.
Matthieu Sozeau
2014-05-06
*
Missing equalities in Names-like structures.
Pierre-Marie Pédrot
2014-03-20
*
Using HMaps in global references.
Pierre-Marie Pédrot
2014-03-08
*
Also use HMaps in KNmap.
Pierre-Marie Pédrot
2014-03-08
*
Using Hashmaps by default in constant and inductive maps. This changes fold and
Pierre-Marie Pédrot
2014-03-07
*
Inductive maps in Environ now use HMap.
Pierre-Marie Pédrot
2014-03-06
*
Lazily computed hash in KerName.t.
Pierre-Marie Pédrot
2014-03-05
*
Fixing generic hashes and replacing them with proper ones.
Pierre-Marie Pédrot
2014-03-03
[next]