aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins
diff options
context:
space:
mode:
authorGravatar Maxime Dénès <mail@maximedenes.fr>2017-12-18 18:57:56 +0100
committerGravatar Maxime Dénès <mail@maximedenes.fr>2017-12-18 18:57:56 +0100
commit7e2f9861f3d38829baf246883e4925d48c9e2998 (patch)
tree17407cece435ac715b7918e1d5abf5e480ae74f6 /plugins
parent6af0969228e57c611e5a0876efe613055de342cd (diff)
parenta60a49f545499f29f067148668b8ec1bc7b55895 (diff)
Merge PR #6406: Make [abstract] nodes show up in the Ltac profile
Diffstat (limited to 'plugins')
-rw-r--r--plugins/ltac/tacinterp.ml10
1 files changed, 7 insertions, 3 deletions
diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml
index 179952f28..ccded4417 100644
--- a/plugins/ltac/tacinterp.ml
+++ b/plugins/ltac/tacinterp.ml
@@ -1158,10 +1158,14 @@ and eval_tactic ist tac : unit Proofview.tactic = match tac with
Proofview.V82.tactic begin
tclSHOWHYPS (Proofview.V82.of_tactic (interp_tactic ist tac))
end
- | TacAbstract (tac,ido) ->
+ | TacAbstract (t,ido) ->
+ let call = LtacMLCall tac in
+ 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
- (Option.map (interp_ident ist (pf_env gl) (project gl)) ido) (interp_tactic ist tac)
- end
+ (Option.map (interp_ident ist (pf_env gl) (project gl)) ido) (interp_tactic ist t)
+ end end)
| TacThen (t1,t) ->
Tacticals.New.tclTHEN (interp_tactic ist t1) (interp_tactic ist t)
| TacDispatch tl ->