diff options
| author |  Amin Timany <amintimany@gmail.com> | 2017-04-01 17:35:39 +0200 |
|---|---|---|
| committer |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-06-16 04:45:19 +0200 |
| commit | fd1f420aef96822bed2ce14214c34e41ceda9b4e (patch) | |
| tree | 50a0e42a1a5a9ab9edc05f6c4a14a2f55df0cbf7 /kernel/safe_typing.ml | |
| parent | 4dd4f186895d16510f217778bb83933be8956082 (diff) | |
Using UInfoInd for universes in inductive types
It stores both universe constraints and subtyping information for
blocks of inductive declarations.
At this stage the there is no inference or checking implemented. The
subtyping information simply encodes equality of levels for the condition of
subtyping.
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 |