diff options
| author | Maxime Dénès | 2017-12-11 09:33:28 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2017-12-11 09:33:28 +0100 |
| commit | 5d52eb47227ed8bd6e67524fc1acc08a95a864fb (patch) | |
| tree | b3a42e7d6d6184f903afd49bb06e3400555ad725 /vernac/command.mli | |
| parent | 42a1e2b6c4b8e4c290ca234211782333b82319bb (diff) | |
| parent | 4f0607dc76d3981fa67ab6231f2817cd1e6134a5 (diff) | |
Merge PR #6369: [api] Remove kernel dependency on intf (Decl_kind)
Diffstat (limited to 'vernac/command.mli')
| -rw-r--r-- | vernac/command.mli | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/vernac/command.mli b/vernac/command.mli index a1f916c782..c7342e6da9 100644 --- a/vernac/command.mli +++ b/vernac/command.mli @@ -82,7 +82,7 @@ type one_inductive_impls = val interp_mutual_inductive : structured_inductive_expr -> decl_notation list -> cumulative_inductive_flag -> - polymorphic -> private_flag -> Decl_kinds.recursivity_kind -> + polymorphic -> private_flag -> Declarations.recursivity_kind -> mutual_inductive_entry * Universes.universe_binders * one_inductive_impls list (** Registering a mutual inductive definition together with its @@ -96,7 +96,7 @@ val declare_mutual_inductive_with_eliminations : val do_mutual_inductive : (one_inductive_expr * decl_notation list) list -> cumulative_inductive_flag -> - polymorphic -> private_flag -> Decl_kinds.recursivity_kind -> unit + polymorphic -> private_flag -> Declarations.recursivity_kind -> unit (** {6 Fixpoints and cofixpoints} *) |