diff options
| author |  Amin Timany <amintimany@gmail.com> | 2017-04-27 20:16:35 +0200 |
|---|---|---|
| committer |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-06-16 04:51:16 +0200 |
| commit | 9468e4b49bd2f397b5e1bd2b7994cc84929fb6ac (patch) | |
| tree | 916f61f35650966d7a288e8579279b0a3e45afc6 /vernac/record.mli | |
| parent | 7b5fcef8a0fb3b97a3980f10596137234061990f (diff) | |
Fix bugs and add an option for cumulativity
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 |