diff options
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/abstract.ml | 2 | ||||
| -rw-r--r-- | tactics/declare.ml | 14 | ||||
| -rw-r--r-- | tactics/declare.mli | 11 | ||||
| -rw-r--r-- | tactics/hints.ml | 2 | ||||
| -rw-r--r-- | tactics/ind_tables.ml | 11 | ||||
| -rw-r--r-- | tactics/ind_tables.mli | 6 | ||||
| -rw-r--r-- | tactics/leminv.ml | 5 |
7 files changed, 24 insertions, 27 deletions
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..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 *) @@ -233,7 +227,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 +235,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 +246,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..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 -> @@ -60,13 +55,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 8526bdd373..e01f3ab961 100644 --- a/tactics/ind_tables.ml +++ b/tactics/ind_tables.ml @@ -22,13 +22,18 @@ open Declarations open Constr open CErrors open Util -open Declare open Decl_kinds 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 = internal_flag -> MutInd.t -> constr array Evd.in_evar_universe_context * Evd.side_effects type individual_scheme_object_function = @@ -131,10 +136,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 id (Declare.DefinitionEntry entry, Decl_kinds.IsDefinition Scheme) in let () = match internal with | InternalTacticRequest -> () - | _-> definition_message id + | _-> Declare.definition_message id in kn, eff 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/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) |