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 /engine | |
| 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 'engine')
| -rw-r--r-- | engine/universes.ml | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/engine/universes.ml b/engine/universes.ml index 955e1d8b5b..ad53bf8981 100644 --- a/engine/universes.ml +++ b/engine/universes.ml @@ -338,14 +338,14 @@ let fresh_constant_instance env c inst = let fresh_inductive_instance env ind inst = let mib, mip = Inductive.lookup_mind_specif env ind in if mib.Declarations.mind_polymorphic then - let inst, ctx = fresh_instance_from mib.Declarations.mind_universes inst in + let inst, ctx = fresh_instance_from (Univ.UInfoInd.univ_context mib.Declarations.mind_universes) inst in ((ind,inst), ctx) else ((ind,Instance.empty), ContextSet.empty) let fresh_constructor_instance env (ind,i) inst = let mib, mip = Inductive.lookup_mind_specif env ind in if mib.Declarations.mind_polymorphic then - let inst, ctx = fresh_instance_from mib.Declarations.mind_universes inst in + let inst, ctx = fresh_instance_from (Univ.UInfoInd.univ_context mib.Declarations.mind_universes) inst in (((ind,i),inst), ctx) else (((ind,i),Instance.empty), ContextSet.empty) @@ -360,14 +360,14 @@ let unsafe_constant_instance env c = let unsafe_inductive_instance env ind = let mib, mip = Inductive.lookup_mind_specif env ind in if mib.Declarations.mind_polymorphic then - let inst, ctx = unsafe_instance_from mib.Declarations.mind_universes in + let inst, ctx = unsafe_instance_from (Univ.UInfoInd.univ_context mib.Declarations.mind_universes) in ((ind,inst), ctx) else ((ind,Instance.empty), UContext.empty) let unsafe_constructor_instance env (ind,i) = let mib, mip = Inductive.lookup_mind_specif env ind in if mib.Declarations.mind_polymorphic then - let inst, ctx = unsafe_instance_from mib.Declarations.mind_universes in + let inst, ctx = unsafe_instance_from (Univ.UInfoInd.univ_context mib.Declarations.mind_universes) in (((ind,i),inst), ctx) else (((ind,i),Instance.empty), UContext.empty) @@ -460,7 +460,7 @@ let type_of_reference env r = | IndRef ind -> let (mib, oib as specif) = Inductive.lookup_mind_specif env ind in if mib.mind_polymorphic then - let inst, ctx = fresh_instance_from mib.mind_universes None in + let inst, ctx = fresh_instance_from (Univ.UInfoInd.univ_context mib.mind_universes) None in let ty = Inductive.type_of_inductive env (specif, inst) in ty, ctx else @@ -469,7 +469,7 @@ let type_of_reference env r = | ConstructRef cstr -> let (mib,oib as specif) = Inductive.lookup_mind_specif env (inductive_of_constructor cstr) in if mib.mind_polymorphic then - let inst, ctx = fresh_instance_from mib.mind_universes None in + let inst, ctx = fresh_instance_from (Univ.UInfoInd.univ_context mib.mind_universes) None in Inductive.type_of_constructor (cstr,inst) specif, ctx else Inductive.type_of_constructor (cstr,Instance.empty) specif, ContextSet.empty |