Make dependence in Declare explicit in tactics.

2 files changed, 10 insertions, 12 deletions

diff --git a/tactics/ind_tables.ml b/tactics/ind_tables.ml
index 8526bdd373..23fa1a312c 100644
--- a/tactics/ind_tables.ml
+++ b/tactics/ind_tables.ml
@@ -22,7 +22,6 @@ open Declarations
 open Constr
 open CErrors
 open Util
-open Declare
 open Decl_kinds
 open Pp
 
@@ -30,9 +29,9 @@ open Pp
 (* Registering schemes in the environment *)
 
 type mutual_scheme_object_function =
-  internal_flag -> MutInd.t -> constr array Evd.in_evar_universe_context * Evd.side_effects
+  Declare.internal_flag -> MutInd.t -> constr array Evd.in_evar_universe_context * Evd.side_effects
 type individual_scheme_object_function =
-  internal_flag -> inductive -> constr Evd.in_evar_universe_context * Evd.side_effects
+  Declare.internal_flag -> inductive -> constr Evd.in_evar_universe_context * Evd.side_effects
 
 type 'a scheme_kind = string
 
@@ -111,8 +110,8 @@ let is_visible_name id =
 
 let compute_name internal id =
   match internal with
-  | UserAutomaticRequest | UserIndividualRequest -> id
-  | InternalTacticRequest ->
+  | Declare.UserAutomaticRequest | Declare.UserIndividualRequest -> id
+  | Declare.InternalTacticRequest ->
       Namegen.next_ident_away_from (add_prefix "internal_" id) is_visible_name
 
 let define internal role id c poly univs =
@@ -131,10 +130,10 @@ let define internal role id c poly univs =
     proof_entry_inline_code = false;
     proof_entry_feedback = None;
   } in
-  let kn, eff = declare_private_constant ~role ~internal id (DefinitionEntry entry, Decl_kinds.IsDefinition Scheme) in
+  let kn, eff = Declare.declare_private_constant ~role ~internal id (Declare.DefinitionEntry entry, Decl_kinds.IsDefinition Scheme) in
   let () = match internal with
-    | InternalTacticRequest -> ()
-    | _-> definition_message id
+    | Declare.InternalTacticRequest -> ()
+    | _-> Declare.definition_message id
   in
   kn, eff
 
@@ -181,7 +180,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=InternalTacticRequest) kind (mind,i as ind) =
+let find_scheme ?(mode=Declare.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/leminv.ml b/tactics/leminv.ml
index d8f4b66d0e..e242b10d33 100644
--- a/tactics/leminv.ml
+++ b/tactics/leminv.ml
@@ -25,7 +25,6 @@ open Reductionops
 open Inductiveops
 open Tacmach.New
 open Clenv
-open Declare
 open Tacticals.New
 open Tactics
 open Decl_kinds
@@ -236,8 +235,8 @@ let inversion_scheme ~name ~poly env sigma t sort dep_option inv_op =
 let add_inversion_lemma ~poly name env sigma t sort dep inv_op =
   let invProof, sigma = inversion_scheme ~name ~poly env sigma t sort dep inv_op in
   let univs = Evd.univ_entry ~poly sigma in
-  let entry = definition_entry ~univs invProof in
-  let _ = declare_constant name (DefinitionEntry entry, IsProof Lemma) in
+  let entry = Declare.definition_entry ~univs invProof in
+  let _ = Declare.declare_constant name (Declare.DefinitionEntry entry, IsProof Lemma) in
   ()
 
 (* inv_op = Inv (derives de complete inv. lemma)