diff options
Diffstat (limited to 'kernel/safe_typing.ml')
| -rw-r--r-- | kernel/safe_typing.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index f5e8e8653..1568fe0bf 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -429,7 +429,7 @@ let globalize_mind_universes mb = if mb.mind_polymorphic then [Now (true, Univ.ContextSet.empty)] else - [Now (false, Univ.ContextSet.of_context mb.mind_universes)] + [Now (false, Univ.ContextSet.of_context (Univ.UInfoInd.univ_context mb.mind_universes))] let constraints_of_sfb env sfb = match sfb with |