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/vconv.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/vconv.ml')
| -rw-r--r-- | kernel/vconv.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/kernel/vconv.ml b/kernel/vconv.ml index 74d956bef..fa1662270 100644 --- a/kernel/vconv.ml +++ b/kernel/vconv.ml @@ -93,7 +93,7 @@ and conv_atom env pb k a1 stk1 a2 stk2 cu = if Environ.polymorphic_ind ind1 env then let mib = Environ.lookup_mind mi env in - let ulen = Univ.UContext.size mib.Declarations.mind_universes in + let ulen = Univ.UContext.size (Univ.UInfoInd.univ_context mib.Declarations.mind_universes) in match stk1 , stk2 with | [], [] -> assert (Int.equal ulen 0); cu | Zapp args1 :: stk1' , Zapp args2 :: stk2' -> |