diff options
| author | Pierre-Marie Pédrot | 2019-06-24 13:30:15 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-06-25 17:52:00 +0200 |
| commit | 8948a2066c7172537a48f49987a79e6bfaab899c (patch) | |
| tree | 105ba019d9e78709a6f2305d0b4cc3102d055a0e /tactics/ind_tables.ml | |
| parent | 803c1dbf2de4e4fe1e447a69b9e5c48d19a72f5f (diff) | |
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.
Diffstat (limited to 'tactics/ind_tables.ml')
| -rw-r--r-- | tactics/ind_tables.ml | 18 |
1 files changed, 12 insertions, 6 deletions
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 |