diff options
| author | Pierre-Marie Pédrot | 2018-11-03 16:27:59 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2018-11-03 16:27:59 +0100 |
| commit | 10e2f279d97b15939e6bdc7658dee20e09b06653 (patch) | |
| tree | e04f05e6ee1efe1abae01ccccb96ecc5e3646088 /plugins/ltac/tacinterp.ml | |
| parent | 228066a783a581ba2b304a12d9fe5e8decebcc48 (diff) | |
| parent | d6619dda80e30adb3d8699c896374657a32ca4e6 (diff) | |
Merge PR #8844: 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 5828494454..2a046a3e65 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) -> |