diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2017-12-18 18:57:56 +0100 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2017-12-18 18:57:56 +0100 |
| commit | 7e2f9861f3d38829baf246883e4925d48c9e2998 (patch) | |
| tree | 17407cece435ac715b7918e1d5abf5e480ae74f6 /plugins/ltac/tacinterp.ml | |
| parent | 6af0969228e57c611e5a0876efe613055de342cd (diff) | |
| parent | a60a49f545499f29f067148668b8ec1bc7b55895 (diff) | |
Merge PR #6406: Make [abstract] nodes show up in the Ltac profile
Diffstat (limited to 'plugins/ltac/tacinterp.ml')
| -rw-r--r-- | plugins/ltac/tacinterp.ml | 10 |
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 -> |