diff options
| author |  Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2017-09-18 14:50:07 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2017-11-24 19:21:18 +0100 |
| commit | 58c0784745f8b2ba7523f246c4611d780c9f3f70 (patch) | |
| tree | fb629961a496e4c84491b4e433a9829621179ca6 /kernel/vconv.ml | |
| parent | 02e6d7f39e3dc2aa8859274bc69b2edf8cc91feb (diff) | |
When declaring constants/inductives use ContextSet if monomorphic.
Also use constant_universes_entry instead of a bool flag to indicate
polymorphism in ParameterEntry.
There are a few places where we convert back to ContextSet because
check_univ_decl returns a UContext, this could be improved.
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 0e452621c..578a89371 100644 --- a/kernel/vconv.ml +++ b/kernel/vconv.ml @@ -93,7 +93,7 @@ and conv_atom env pb k a1 stk1 a2 stk2 cu = let mib = Environ.lookup_mind mi env in let ulen = match mib.Declarations.mind_universes with - | Declarations.Monomorphic_ind ctx -> Univ.UContext.size ctx + | Declarations.Monomorphic_ind ctx -> Univ.ContextSet.size ctx | Declarations.Polymorphic_ind auctx -> Univ.AUContext.size auctx | Declarations.Cumulative_ind cumi -> Univ.AUContext.size (Univ.ACumulativityInfo.univ_context cumi) |