From 44f462aa380de847452c0809d15c86649d5d6a7a Mon Sep 17 00:00:00 2001 From: Amin Timany Date: Tue, 28 Mar 2017 19:24:02 +0200 Subject: Extend definition of inductives to include subtyping info --- vernac/record.mli | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) (limited to 'vernac/record.mli') diff --git a/vernac/record.mli b/vernac/record.mli index 3fd651db9..a380b041a 100644 --- a/vernac/record.mli +++ b/vernac/record.mli @@ -26,7 +26,8 @@ val declare_projections : val declare_structure : Decl_kinds.recursivity_kind -> - bool (** polymorphic?*) -> Univ.universe_context -> + bool (** polymorphic?*) -> + (Univ.universe_context * Univ.universe_context) (** universe and subtyping constraints *) -> Id.t -> Id.t -> manual_explicitation list -> Context.Rel.t -> (** params *) constr -> (** arity *) bool (** template arity ? *) -> -- cgit v1.2.3