diff options
| author | Pierre-Marie Pédrot | 2019-05-14 20:27:24 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-05-19 13:14:19 +0200 |
| commit | 93aa8aad110a2839d16dce53af12f0728b59ed2a (patch) | |
| tree | 3bf17f844a44f5010773a0857c53ce99c05835a6 /tactics/abstract.ml | |
| parent | b1a3ea4855b1e150b2e677a6d5466458893d6c60 (diff) | |
Merge the definition of constants and private constants in the API.
Diffstat (limited to 'tactics/abstract.ml')
| -rw-r--r-- | tactics/abstract.ml | 5 |
1 files changed, 2 insertions, 3 deletions
diff --git a/tactics/abstract.ml b/tactics/abstract.ml index 499152f39a..6dd9a976f9 100644 --- a/tactics/abstract.ml +++ b/tactics/abstract.ml @@ -158,9 +158,9 @@ 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_constant ~internal:Declare.InternalTacticRequest ~local:true id decl + Declare.declare_private_constant ~role:Entries.Subproof ~internal:Declare.InternalTacticRequest ~local:true id decl in - let cst = Impargs.with_implicit_protection cst () in + let cst, eff = Impargs.with_implicit_protection cst () in let inst = match const.Entries.const_entry_universes with | Entries.Monomorphic_entry _ -> EInstance.empty | Entries.Polymorphic_entry (_, ctx) -> @@ -174,7 +174,6 @@ let cache_term_by_tactic_then ~opaque ~name_op ?(goal_type=None) tac tacK = let lem = mkConstU (cst, inst) in let evd = Evd.set_universe_context evd ectx in let open Safe_typing in - let eff = private_constant (Global.safe_env ()) Entries.Subproof cst in let effs = concat_private eff Entries.(snd (Future.force const.const_entry_body)) in let solve = |