diff options
author | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-07-10 18:05:23 +0200 |
---|---|---|
committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-07-11 14:50:47 +0200 |
commit | b8a7222e670f69e024d50394afd88204e15d1b29 (patch) | |
tree | 90c3c75ca9c2647ad41c6a30954cdf8ce3f6b5d8 /library/global.ml | |
parent | 1309723672def9bf322a23e9c789e4a8bc2a4ac3 (diff) |
Less footguns in universe handling: remove subst_instance_context.
This function was lurking around, waiting to bite anybody willing to use it.
We use instead a better API, correct and much less error-prone.
Diffstat (limited to 'library/global.ml')
0 files changed, 0 insertions, 0 deletions