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 /kernel/environ.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 'kernel/environ.ml')
| -rw-r--r-- | kernel/environ.ml | 3 |
1 files changed, 1 insertions, 2 deletions
diff --git a/kernel/environ.ml b/kernel/environ.ml index dd204c7d5..ca2c8e135 100644 --- a/kernel/environ.ml +++ b/kernel/environ.ml @@ -230,8 +230,7 @@ let add_constant kn cb env = let constraints_of cb u = match cb.const_universes with | Monomorphic_const _ -> Univ.Constraint.empty - | Polymorphic_const ctx -> - Univ.UContext.constraints (Univ.subst_instance_context u ctx) + | Polymorphic_const ctx -> Univ.AUContext.instantiate u ctx let map_regular_arity f = function | RegularArity a as ar -> |