diff options
| author | Hugo Herbelin | 2018-10-09 20:22:59 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2018-10-19 16:52:55 +0200 |
| commit | df6b72e348543a289a2ef3f89f32c905add564bc (patch) | |
| tree | 3fc74e3474457f12a9cd4975707c67553b3e6db1 /_CoqProject | |
| parent | 988aab80e03e593c76869b113c5bcc043209d952 (diff) | |
Moving Global.type_of_global_in_context to Typeops.
It is purely functional, so no need for it to be in global now that
GlobRef.t are in the kernel.
Also updated the comments.
Diffstat (limited to '_CoqProject')
0 files changed, 0 insertions, 0 deletions