diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2017-12-18 10:27:13 +0100 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2017-12-18 10:27:13 +0100 |
| commit | 32acb87d4b6b53b26a891b93df6244e0446411b0 (patch) | |
| tree | 64c4bcc2a6410a27c199c84b3f51e8ac79d67837 /plugins/ltac/tacinterp.ml | |
| parent | 3da76841125ef48889c8eceb134116e2d0bd7a2e (diff) | |
| parent | 79e97ce799d35c1082ccc1a57468f8bb4f8efe42 (diff) | |
Merge PR #6411: Fix #5081 by more fine-grained LtacProf recording
Diffstat (limited to 'plugins/ltac/tacinterp.ml')
| -rw-r--r-- | plugins/ltac/tacinterp.ml | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml index ded902a8f..179952f28 100644 --- a/plugins/ltac/tacinterp.ml +++ b/plugins/ltac/tacinterp.ml @@ -1272,7 +1272,8 @@ and interp_ltac_reference ?loc' mustbetac ist r : Val.t Ftactic.t = let extra = TacStore.set extra f_trace trace in let ist = { lfun = Id.Map.empty; extra = extra; } in let appl = GlbAppl[r,[]] in - val_interp ~appl ist (Tacenv.interp_ltac r) + Profile_ltac.do_profile "interp_ltac_reference" trace ~count_call:false + (val_interp ~appl ist (Tacenv.interp_ltac r)) and interp_tacarg ist arg : Val.t Ftactic.t = match arg with @@ -1338,7 +1339,8 @@ and interp_app loc ist fv largs : Val.t Ftactic.t = let ist = { lfun = newlfun; extra = TacStore.set ist.extra f_trace []; } in - catch_error_tac trace (val_interp ist body) >>= fun v -> + Profile_ltac.do_profile "interp_app" trace ~count_call:false + (catch_error_tac trace (val_interp ist body)) >>= fun v -> Ftactic.return (name_vfun (push_appl appl largs) v) end begin fun (e, info) -> |