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. --- vernac/record.mli | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'vernac/record.mli') diff --git a/vernac/record.mli b/vernac/record.mli index a380b041a..ec5d2cf83 100644 --- a/vernac/record.mli +++ b/vernac/record.mli @@ -27,7 +27,7 @@ val declare_projections : val declare_structure : Decl_kinds.recursivity_kind -> bool (** polymorphic?*) -> - (Univ.universe_context * Univ.universe_context) (** universe and subtyping constraints *) -> + Univ.universe_info_ind (** universe and subtyping constraints *) -> Id.t -> Id.t -> manual_explicitation list -> Context.Rel.t -> (** params *) constr -> (** arity *) bool (** template arity ? *) -> -- cgit v1.2.3