From 82bccc5d62cbdcf0d79d8a85c98ca19823a33629 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Mon, 24 Jun 2019 13:22:28 +0200 Subject: Make dependence in Declare explicit in tactics. --- tactics/ind_tables.ml | 17 ++++++++--------- tactics/leminv.ml | 5 ++--- 2 files changed, 10 insertions(+), 12 deletions(-) (limited to 'tactics') 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) -- cgit v1.2.3 From 803c1dbf2de4e4fe1e447a69b9e5c48d19a72f5f Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Mon, 24 Jun 2019 13:24:05 +0200 Subject: Remove the internal_flag argument from Declare API. It was never used actually. --- tactics/abstract.ml | 2 +- tactics/declare.ml | 8 ++++---- tactics/declare.mli | 6 +++--- tactics/hints.ml | 2 +- tactics/ind_tables.ml | 2 +- 5 files changed, 10 insertions(+), 10 deletions(-) (limited to 'tactics') diff --git a/tactics/abstract.ml b/tactics/abstract.ml index 465f736032..662a2fc22c 100644 --- a/tactics/abstract.ml +++ b/tactics/abstract.ml @@ -158,7 +158,7 @@ let cache_term_by_tactic_then ~opaque ~name_op ?(goal_type=None) tac tacK = (* do not compute the implicit arguments, it may be costly *) let () = Impargs.make_implicit_args false in (* ppedrot: seems legit to have abstracted subproofs as local*) - Declare.declare_private_constant ~internal:Declare.InternalTacticRequest ~local:Declare.ImportNeedQualified name decl + Declare.declare_private_constant ~local:Declare.ImportNeedQualified name decl in let cst, eff = Impargs.with_implicit_protection cst () in let inst = match const.Proof_global.proof_entry_universes with diff --git a/tactics/declare.ml b/tactics/declare.ml index 4a4e2cf60a..27c2d089f6 100644 --- a/tactics/declare.ml +++ b/tactics/declare.ml @@ -233,7 +233,7 @@ let define_constant ~side_effect id cd = let kn, eff = Global.add_constant ~side_effect ~in_section id decl in kn, eff, export -let declare_constant ?(internal = UserIndividualRequest) ?(local = ImportDefaultBehavior) id (cd, kind) = +let declare_constant ?(local = ImportDefaultBehavior) id (cd, kind) = let () = check_exists id in let kn, (), export = define_constant ~side_effect:PureEntry id cd in (* Register the libobjects attached to the constants and its subproofs *) @@ -241,7 +241,7 @@ let declare_constant ?(internal = UserIndividualRequest) ?(local = ImportDefault let () = register_constant kn kind local in kn -let declare_private_constant ?role ?(internal=UserIndividualRequest) ?(local = ImportDefaultBehavior) id (cd, kind) = +let declare_private_constant ?role ?(local = ImportDefaultBehavior) id (cd, kind) = let kn, eff, export = define_constant ~side_effect:EffectEntry id cd in let () = assert (List.is_empty export) in let () = register_constant kn kind local in @@ -252,13 +252,13 @@ let declare_private_constant ?role ?(internal=UserIndividualRequest) ?(local = I let eff = { Evd.seff_private = eff; Evd.seff_roles; } in kn, eff -let declare_definition ?(internal=UserIndividualRequest) +let declare_definition ?(opaque=false) ?(kind=Decl_kinds.Definition) ?(local = ImportDefaultBehavior) id ?types (body,univs) = let cb = definition_entry ?types ~univs ~opaque body in - declare_constant ~internal ~local id + declare_constant ~local id (DefinitionEntry cb, Decl_kinds.IsDefinition kind) (** Declaration of section variables and local definitions *) diff --git a/tactics/declare.mli b/tactics/declare.mli index d87c096119..495f66c745 100644 --- a/tactics/declare.mli +++ b/tactics/declare.mli @@ -60,13 +60,13 @@ type import_status = ImportDefaultBehavior | ImportNeedQualified internal specify if the constant has been created by the kernel or by the user, and in the former case, if its errors should be silent *) val declare_constant : - ?internal:internal_flag -> ?local:import_status -> Id.t -> constant_declaration -> Constant.t + ?local:import_status -> Id.t -> constant_declaration -> Constant.t val declare_private_constant : - ?role:Evd.side_effect_role -> ?internal:internal_flag -> ?local:import_status -> Id.t -> constant_declaration -> Constant.t * Evd.side_effects + ?role:Evd.side_effect_role -> ?local:import_status -> Id.t -> constant_declaration -> Constant.t * Evd.side_effects val declare_definition : - ?internal:internal_flag -> ?opaque:bool -> ?kind:definition_object_kind -> + ?opaque:bool -> ?kind:definition_object_kind -> ?local:import_status -> Id.t -> ?types:constr -> constr Entries.in_universes_entry -> Constant.t diff --git a/tactics/hints.ml b/tactics/hints.ml index 014e54158d..3a3a6b94dc 100644 --- a/tactics/hints.ml +++ b/tactics/hints.ml @@ -1320,7 +1320,7 @@ let project_hint ~poly pri l2r r = in let ctx = Evd.univ_entry ~poly sigma in let c = EConstr.to_constr sigma c in - let c = Declare.declare_definition ~internal:Declare.InternalTacticRequest id (c,ctx) in + let c = Declare.declare_definition id (c,ctx) in let info = {Typeclasses.hint_priority = pri; hint_pattern = None} in (info,false,true,PathAny, IsGlobRef (Globnames.ConstRef c)) diff --git a/tactics/ind_tables.ml b/tactics/ind_tables.ml index 23fa1a312c..d5e88791a6 100644 --- a/tactics/ind_tables.ml +++ b/tactics/ind_tables.ml @@ -130,7 +130,7 @@ let define internal role id c poly univs = proof_entry_inline_code = false; proof_entry_feedback = None; } in - let kn, eff = Declare.declare_private_constant ~role ~internal id (Declare.DefinitionEntry entry, Decl_kinds.IsDefinition Scheme) in + let kn, eff = Declare.declare_private_constant ~role id (Declare.DefinitionEntry entry, Decl_kinds.IsDefinition Scheme) in let () = match internal with | Declare.InternalTacticRequest -> () | _-> Declare.definition_message id -- cgit v1.2.3 From 8948a2066c7172537a48f49987a79e6bfaab899c Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Mon, 24 Jun 2019 13:30:15 +0200 Subject: 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. --- tactics/declare.ml | 6 ------ tactics/declare.mli | 5 ----- tactics/ind_tables.ml | 18 ++++++++++++------ tactics/ind_tables.mli | 6 +++++- 4 files changed, 17 insertions(+), 18 deletions(-) (limited to 'tactics') 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 = -- cgit v1.2.3