diff options
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/ltac/extratactics.mlg | 4 | ||||
| -rw-r--r-- | plugins/ltac/tacinterp.ml | 2 |
2 files changed, 3 insertions, 3 deletions
diff --git a/plugins/ltac/extratactics.mlg b/plugins/ltac/extratactics.mlg index b660865e8b..05a65e4cd8 100644 --- a/plugins/ltac/extratactics.mlg +++ b/plugins/ltac/extratactics.mlg @@ -855,9 +855,9 @@ END TACTIC EXTEND transparent_abstract | [ "transparent_abstract" tactic3(t) ] -> { Proofview.Goal.enter begin fun gl -> - Tactics.tclABSTRACT ~opaque:false None (Tacinterp.tactic_of_value ist t) end } + Abstract.tclABSTRACT ~opaque:false None (Tacinterp.tactic_of_value ist t) end } | [ "transparent_abstract" tactic3(t) "using" ident(id) ] -> { Proofview.Goal.enter begin fun gl -> - Tactics.tclABSTRACT ~opaque:false (Some id) (Tacinterp.tactic_of_value ist t) end } + Abstract.tclABSTRACT ~opaque:false (Some id) (Tacinterp.tactic_of_value ist t) end } END (* ********************************************************************* *) diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml index b60b77595b..eecb2ac6de 100644 --- a/plugins/ltac/tacinterp.ml +++ b/plugins/ltac/tacinterp.ml @@ -1078,7 +1078,7 @@ and eval_tactic ist tac : unit Proofview.tactic = match tac with push_trace(None,call) ist >>= fun trace -> Profile_ltac.do_profile "eval_tactic:TacAbstract" trace (catch_error_tac trace begin - Proofview.Goal.enter begin fun gl -> Tactics.tclABSTRACT + Proofview.Goal.enter begin fun gl -> Abstract.tclABSTRACT (Option.map (interp_ident ist (pf_env gl) (project gl)) ido) (interp_tactic ist t) end end) | TacThen (t1,t) -> |