diff options
| author | Emilio Jesus Gallego Arias | 2019-06-06 13:21:48 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2019-06-24 20:55:09 +0200 |
| commit | b2aae7ba35a90e695d34f904c74f5156385344a9 (patch) | |
| tree | 20ab3a596f00e587309a578d5ba18689076a2185 /tactics | |
| parent | 8b903319eae4d645f9385e8280d04d18a4f3a2bc (diff) | |
[api] Move `locality` from `library` to `vernac`.
This datatype does belong to this layer.
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/abstract.ml | 8 | ||||
| -rw-r--r-- | tactics/declare.ml | 2 | ||||
| -rw-r--r-- | tactics/declare.mli | 2 |
3 files changed, 8 insertions, 4 deletions
diff --git a/tactics/abstract.ml b/tactics/abstract.ml index 4ea5b676fb..465f736032 100644 --- a/tactics/abstract.ml +++ b/tactics/abstract.ml @@ -102,9 +102,9 @@ let cache_term_by_tactic_then ~opaque ~name_op ?(goal_type=None) tac tacK = redundancy on constant declaration. This opens up an interesting question, how does abstract behave when discharge is local for example? *) - let scope, suffix = if opaque - then Global ImportDefaultBehavior, "_subproof" - else Global ImportDefaultBehavior, "_subterm" in + let suffix = if opaque + then "_subproof" + else "_subterm" in let name = name_op_to_name ~name_op ~name suffix in Proofview.Goal.enter begin fun gl -> let env = Proofview.Goal.env gl in @@ -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:ImportNeedQualified name decl + Declare.declare_private_constant ~internal:Declare.InternalTacticRequest ~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 ca5d265733..02253e70bf 100644 --- a/tactics/declare.ml +++ b/tactics/declare.ml @@ -33,6 +33,8 @@ type internal_flag = | InternalTacticRequest (* kernel action, no message is displayed *) | UserIndividualRequest (* user action, a message is displayed *) +type import_status = ImportDefaultBehavior | ImportNeedQualified + (** Declaration of constants and parameters *) type constant_obj = { diff --git a/tactics/declare.mli b/tactics/declare.mli index 0a2332748c..bdb5af7430 100644 --- a/tactics/declare.mli +++ b/tactics/declare.mli @@ -51,6 +51,8 @@ val definition_entry : ?fix_exn:Future.fix_exn -> ?univs:Entries.universes_entry -> ?eff:Evd.side_effects -> constr -> Evd.side_effects Proof_global.proof_entry +type import_status = ImportDefaultBehavior | ImportNeedQualified + (** [declare_constant id cd] declares a global declaration (constant/parameter) with name [id] in the current section; it returns the full path of the declaration |