diff options
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/safe_typing.ml | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index 97b74cadb9..e0a07dcc3a 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -254,7 +254,9 @@ let universes_of_private eff = if cb.const_polymorphic then acc else (Univ.ContextSet.of_context cb.const_universes) :: acc) acc l - | Entries.SEsubproof _ -> acc) + | Entries.SEsubproof (c, cb, e) -> + if cb.const_polymorphic then acc + else Univ.ContextSet.of_context cb.const_universes :: acc) [] eff let env_of_safe_env senv = senv.env |