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 /pretyping | |
| 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 'pretyping')
| -rw-r--r-- | pretyping/typeclasses.ml | 2 | ||||
| -rw-r--r-- | pretyping/vnorm.ml | 2 |
2 files changed, 2 insertions, 2 deletions
diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml index d7b4842810..152ccb0798 100644 --- a/pretyping/typeclasses.ml +++ b/pretyping/typeclasses.ml @@ -123,7 +123,7 @@ let typeclass_univ_instance (cl,u') = else Univ.Instance.empty | IndRef c -> let mib,oib = Global.lookup_inductive c in - if mib.mind_polymorphic then Univ.UContext.instance mib.mind_universes + if mib.mind_polymorphic then Univ.UContext.instance (Univ.UInfoInd.univ_context mib.mind_universes) else Univ.Instance.empty | _ -> Univ.Instance.empty in Array.fold_left2 (fun subst u u' -> Univ.LMap.add u u' subst) diff --git a/pretyping/vnorm.ml b/pretyping/vnorm.ml index b08666483e..074b7373c7 100644 --- a/pretyping/vnorm.ml +++ b/pretyping/vnorm.ml @@ -174,7 +174,7 @@ and nf_whd env sigma whd typ = | Vatom_stk(Aind ((mi,i) as ind), stk) -> let mib = Environ.lookup_mind mi env in let nb_univs = - if mib.mind_polymorphic then Univ.UContext.size mib.mind_universes + if mib.mind_polymorphic then Univ.UContext.size (Univ.UInfoInd.univ_context mib.mind_universes) else 0 in let mk u = |