diff options
| author | Amin Timany | 2017-04-01 17:35:39 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2017-06-16 04:45:19 +0200 |
| commit | fd1f420aef96822bed2ce14214c34e41ceda9b4e (patch) | |
| tree | 50a0e42a1a5a9ab9edc05f6c4a14a2f55df0cbf7 /kernel/declareops.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/declareops.ml')
| -rw-r--r-- | kernel/declareops.ml | 7 |
1 files changed, 3 insertions, 4 deletions
diff --git a/kernel/declareops.ml b/kernel/declareops.ml index 47a23c8555..cdea468adf 100644 --- a/kernel/declareops.ml +++ b/kernel/declareops.ml @@ -261,19 +261,18 @@ let subst_mind_body sub mib = mind_packets = Array.smartmap (subst_mind_packet sub) mib.mind_packets ; mind_polymorphic = mib.mind_polymorphic; mind_universes = mib.mind_universes; - mind_subtyping = mib.mind_subtyping; mind_private = mib.mind_private; mind_typing_flags = mib.mind_typing_flags; } let inductive_instance mib = if mib.mind_polymorphic then - Univ.UContext.instance mib.mind_universes + Univ.UContext.instance (Univ.UInfoInd.univ_context mib.mind_universes) else Univ.Instance.empty let inductive_context mib = if mib.mind_polymorphic then - Univ.instantiate_univ_context mib.mind_universes + Univ.instantiate_univ_context (Univ.UInfoInd.univ_context mib.mind_universes) else Univ.UContext.empty (** {6 Hash-consing of inductive declarations } *) @@ -306,7 +305,7 @@ let hcons_mind mib = { mib with mind_packets = Array.smartmap hcons_mind_packet mib.mind_packets; mind_params_ctxt = hcons_rel_context mib.mind_params_ctxt; - mind_universes = Univ.hcons_universe_context mib.mind_universes } + mind_universes = Univ.hcons_universe_info_ind mib.mind_universes } (** {6 Stm machinery } *) |