diff options
| author | Hugo Herbelin | 2018-10-09 20:46:15 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2018-10-19 16:52:55 +0200 |
| commit | 09d0ba708a96125632344f2f994b45e9075fc303 (patch) | |
| tree | 73cb5365417f4ac92c958e66aa61bab766ba44ec /plugins | |
| parent | df6b72e348543a289a2ef3f89f32c905add564bc (diff) | |
Moving Global.constr_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.
Diffstat (limited to 'plugins')
0 files changed, 0 insertions, 0 deletions