diff options
Diffstat (limited to 'vernac/record.mli')
-rw-r--r-- | vernac/record.mli | 7 |
1 files changed, 4 insertions, 3 deletions
diff --git a/vernac/record.mli b/vernac/record.mli index ec5d2cf83..c43d833b0 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?*) -> + Decl_kinds.cumulative_inductive_flag -> + Decl_kinds.polymorphic -> Univ.universe_info_ind (** universe and subtyping constraints *) -> Id.t -> Id.t -> manual_explicitation list -> Context.Rel.t -> (** params *) constr -> (** arity *) @@ -39,8 +40,8 @@ val declare_structure : inductive val definition_structure : - inductive_kind * Decl_kinds.polymorphic * Decl_kinds.recursivity_kind * - plident with_coercion * local_binder_expr list * + inductive_kind * Decl_kinds.cumulative_inductive_flag * Decl_kinds.polymorphic * + Decl_kinds.recursivity_kind * plident with_coercion * local_binder_expr list * (local_decl_expr with_instance with_priority with_notation) list * Id.t * constr_expr option -> global_reference |