diff options
Diffstat (limited to 'toplevel/record.mli')
| -rw-r--r-- | toplevel/record.mli | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/toplevel/record.mli b/toplevel/record.mli index 564d4409f..0e23af5c0 100644 --- a/toplevel/record.mli +++ b/toplevel/record.mli @@ -27,7 +27,8 @@ val declare_projections : bool list -> manual_explicitation list list -> rel_context -> (name * bool) list * constant option list -val declare_structure : bool (*coinductive?*)-> bool (*infer?*) -> identifier -> identifier -> +val declare_structure : Decl_kinds.recursivity_kind -> + bool (*infer?*) -> identifier -> identifier -> manual_explicitation list -> rel_context -> (* params *) constr -> (* arity *) Impargs.manual_explicitation list list -> rel_context -> (* fields *) ?kind:Decl_kinds.definition_object_kind -> ?name:identifier -> @@ -37,6 +38,6 @@ val declare_structure : bool (*coinductive?*)-> bool (*infer?*) -> identifier -> inductive val definition_structure : - record_kind * bool (*coinductive?*) * bool(*infer?*)* lident with_coercion * local_binder list * + inductive_kind * Decl_kinds.recursivity_kind * bool(*infer?*)* lident with_coercion * local_binder list * (local_decl_expr with_coercion with_notation) list * identifier * constr_expr option -> global_reference |