diff options
| author | Pierre-Marie Pédrot | 2019-06-24 13:22:28 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-06-25 17:48:49 +0200 |
| commit | 82bccc5d62cbdcf0d79d8a85c98ca19823a33629 (patch) | |
| tree | c770a1742323e451799ff1be5da7b60bec4cadd3 /tactics/ind_tables.ml | |
| parent | 7dfcb0f7c817e66280ab37b6c653b5596a16c249 (diff) | |
Make dependence in Declare explicit in tactics.
Diffstat (limited to 'tactics/ind_tables.ml')
| -rw-r--r-- | tactics/ind_tables.ml | 17 |
1 files changed, 8 insertions, 9 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 |