aboutsummaryrefslogtreecommitdiffhomepage
path: root/intf/vernacexpr.ml
diff options
context:
space:
mode:
Diffstat (limited to 'intf/vernacexpr.ml')
-rw-r--r--intf/vernacexpr.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/intf/vernacexpr.ml b/intf/vernacexpr.ml
index 5c9141fd6..8deddaa5d 100644
--- a/intf/vernacexpr.ml
+++ b/intf/vernacexpr.ml
@@ -145,7 +145,7 @@ type coercion_flag = bool (* true = AddCoercion false = NoCoercion *)
type instance_flag = bool option
(* Some true = Backward instance; Some false = Forward instance, None = NoInstance *)
type export_flag = bool (* true = Export; false = Import *)
-type inductive_flag = Decl_kinds.recursivity_kind
+type inductive_flag = Declarations.recursivity_kind
type onlyparsing_flag = Flags.compat_version option
(* Some v = Parse only; None = Print also.
If v<>Current, it contains the name of the coq version