diff options
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/abstract.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/tactics/abstract.ml b/tactics/abstract.ml index a5b2f99457..e91fe5067c 100644 --- a/tactics/abstract.ml +++ b/tactics/abstract.ml @@ -103,8 +103,8 @@ let cache_term_by_tactic_then ~opaque ~name_op ?(goal_type=None) tac tacK = question, how does abstract behave when discharge is local for example? *) let goal_kind, suffix = if opaque - then (Global,poly,Proof Theorem), "_subproof" - else (Global,poly,DefinitionBody Definition), "_subterm" in + then (Global ImportDefaultBehavior,poly,Proof Theorem), "_subproof" + else (Global ImportDefaultBehavior,poly,DefinitionBody Definition), "_subterm" in let id, goal_kind = name_op_to_name ~name_op ~name ~goal_kind 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 ~role:Entries.Subproof ~internal:Declare.InternalTacticRequest ~local:true id decl + Declare.declare_private_constant ~role:Entries.Subproof ~internal:Declare.InternalTacticRequest ~local:ImportNeedQualified id decl in let cst, eff = Impargs.with_implicit_protection cst () in let inst = match const.Entries.const_entry_universes with |