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 /interp/notation.ml | |
| 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 'interp/notation.ml')
0 files changed, 0 insertions, 0 deletions