diff options
| author | Gaëtan Gilbert | 2018-10-29 14:34:39 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2018-10-30 13:04:18 +0100 |
| commit | 82105f030e13aebcb232eb912526ff8ca0650a24 (patch) | |
| tree | 9839e8698063b8e55f4255efdabcceed2e8deea3 /plugins/ltac/tacinterp.ml | |
| parent | 0ac673e562c34245e4e48efc428d808e917be79b (diff) | |
Move abstract out of tactics.ml
Diffstat (limited to 'plugins/ltac/tacinterp.ml')
| -rw-r--r-- | plugins/ltac/tacinterp.ml | 2 |
1 files changed, 1 insertions, 1 deletions
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) -> |