From fd1f420aef96822bed2ce14214c34e41ceda9b4e Mon Sep 17 00:00:00 2001 From: Amin Timany Date: Sat, 1 Apr 2017 17:35:39 +0200 Subject: 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. --- kernel/term_typing.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'kernel/term_typing.ml') diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml index bdfd00a8d..3cf2299d8 100644 --- a/kernel/term_typing.ml +++ b/kernel/term_typing.ml @@ -313,7 +313,7 @@ let infer_declaration ~trust env kn dcl = in let term, typ = pb.proj_eta in Def (Mod_subst.from_val (hcons_constr term)), RegularArity typ, Some pb, - mib.mind_polymorphic, mib.mind_universes, false, None + mib.mind_polymorphic, Univ.UInfoInd.univ_context mib.mind_universes, false, None let global_vars_set_constant_type env = function | RegularArity t -> global_vars_set env t -- cgit v1.2.3