diff options
| author | Matthieu Sozeau | 2015-10-29 15:09:14 -0400 |
|---|---|---|
| committer | Matthieu Sozeau | 2015-10-29 15:18:16 -0400 |
| commit | 78edfe09f34db4a28fb41a1f6fd3bb4922d09ec8 (patch) | |
| tree | 7352b064e999688b44b052b4593b48457e54a27c | |
| parent | 7f8a31e21edd533ba12399b7ee5647ef30e38fe5 (diff) | |
Collect subproof universes in handle_side_effects.
| -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 |