aboutsummaryrefslogtreecommitdiffhomepage
path: root/vernac/command.mli
diff options
context:
space:
mode:
Diffstat (limited to 'vernac/command.mli')
-rw-r--r--vernac/command.mli4
1 files changed, 2 insertions, 2 deletions
diff --git a/vernac/command.mli b/vernac/command.mli
index a1f916c78..c7342e6da 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} *)