Move the internal_flag type from Declare to Ind_tables.

It is completely local to that file, there was no point to put it into
the unrelated Declare file.

5 files changed, 20 insertions, 21 deletions

diff --git a/tactics/declare.ml b/tactics/declare.ml
index 27c2d089f6..668026500d 100644
--- a/tactics/declare.ml
+++ b/tactics/declare.ml
@@ -27,12 +27,6 @@ open Cooking
 open Decls
 open Decl_kinds
 
-(** flag for internal message display *)
-type internal_flag =
-  | UserAutomaticRequest (* kernel action, a message is displayed *)
-  | InternalTacticRequest  (* kernel action, no message is displayed *)
-  | UserIndividualRequest   (* user action, a message is displayed *)
-
 type import_status = ImportDefaultBehavior | ImportNeedQualified
 
 (** Declaration of constants and parameters *)
diff --git a/tactics/declare.mli b/tactics/declare.mli
index 495f66c745..1f72fff30e 100644
--- a/tactics/declare.mli
+++ b/tactics/declare.mli
@@ -40,11 +40,6 @@ val declare_variable : variable -> variable_declaration -> Libobject.object_name
 
 type constant_declaration = Evd.side_effects constant_entry * logical_kind
 
-type internal_flag =
-  | UserAutomaticRequest
-  | InternalTacticRequest
-  | UserIndividualRequest
-
 (* Default definition entries, transparent with no secctx or proj information *)
 val definition_entry : ?fix_exn:Future.fix_exn ->
   ?opaque:bool -> ?inline:bool -> ?types:types ->
diff --git a/tactics/ind_tables.ml b/tactics/ind_tables.ml
index d5e88791a6..e01f3ab961 100644
--- a/tactics/ind_tables.ml
+++ b/tactics/ind_tables.ml
@@ -28,10 +28,16 @@ open Pp
 (**********************************************************************)
 (* Registering schemes in the environment *)
 
+(** flag for internal message display *)
+type internal_flag =
+  | UserAutomaticRequest (* kernel action, a message is displayed *)
+  | InternalTacticRequest  (* kernel action, no message is displayed *)
+  | UserIndividualRequest   (* user action, a message is displayed *)
+
 type mutual_scheme_object_function =
-  Declare.internal_flag -> MutInd.t -> constr array Evd.in_evar_universe_context * Evd.side_effects
+  internal_flag -> MutInd.t -> constr array Evd.in_evar_universe_context * Evd.side_effects
 type individual_scheme_object_function =
-  Declare.internal_flag -> inductive -> constr Evd.in_evar_universe_context * Evd.side_effects
+  internal_flag -> inductive -> constr Evd.in_evar_universe_context * Evd.side_effects
 
 type 'a scheme_kind = string
 
@@ -110,8 +116,8 @@ let is_visible_name id =
 
 let compute_name internal id =
   match internal with
-  | Declare.UserAutomaticRequest | Declare.UserIndividualRequest -> id
-  | Declare.InternalTacticRequest ->
+  | UserAutomaticRequest | UserIndividualRequest -> id
+  | InternalTacticRequest ->
       Namegen.next_ident_away_from (add_prefix "internal_" id) is_visible_name
 
 let define internal role id c poly univs =
@@ -132,7 +138,7 @@ let define internal role id c poly univs =
   } in
   let kn, eff = Declare.declare_private_constant ~role id (Declare.DefinitionEntry entry, Decl_kinds.IsDefinition Scheme) in
   let () = match internal with
-    | Declare.InternalTacticRequest -> ()
+    | InternalTacticRequest -> ()
     | _-> Declare.definition_message id
   in
   kn, eff
@@ -180,7 +186,7 @@ let find_scheme_on_env_too kind ind =
   let s = String.Map.find kind (Indmap.find ind !scheme_map) in
   s, Evd.empty_side_effects
 
-let find_scheme ?(mode=Declare.InternalTacticRequest) kind (mind,i as ind) =
+let find_scheme ?(mode=InternalTacticRequest) kind (mind,i as ind) =
   try find_scheme_on_env_too kind ind
   with Not_found ->
   match Hashtbl.find scheme_object_table kind with
diff --git a/tactics/ind_tables.mli b/tactics/ind_tables.mli
index 109fb64b2b..17e9c7ef42 100644
--- a/tactics/ind_tables.mli
+++ b/tactics/ind_tables.mli
@@ -10,7 +10,6 @@
 
 open Names
 open Constr
-open Declare
 
 (** This module provides support for registering inductive scheme builders,
    declaring schemes and generating schemes on demand *)
@@ -21,6 +20,11 @@ type mutual
 type individual
 type 'a scheme_kind
 
+type internal_flag =
+  | UserAutomaticRequest
+  | InternalTacticRequest
+  | UserIndividualRequest
+
 type mutual_scheme_object_function =
   internal_flag -> MutInd.t -> constr array Evd.in_evar_universe_context * Evd.side_effects
 type individual_scheme_object_function =
diff --git a/vernac/auto_ind_decl.ml b/vernac/auto_ind_decl.ml
index 8b98408c5e..9b96fbf68a 100644
--- a/vernac/auto_ind_decl.ml
+++ b/vernac/auto_ind_decl.ml
@@ -676,9 +676,9 @@ repeat ( apply andb_prop in z;let z1:= fresh "Z" in destruct z as [z1 z]).
 let bl_scheme_kind_aux = ref (fun _ -> failwith "Undefined")
 
 let side_effect_of_mode = function
-  | Declare.UserAutomaticRequest -> false
-  | Declare.InternalTacticRequest -> true
-  | Declare.UserIndividualRequest -> false
+  | UserAutomaticRequest -> false
+  | InternalTacticRequest -> true
+  | UserIndividualRequest -> false
 
 let make_bl_scheme mode mind =
   let mib = Global.lookup_mind mind in