Make [abstract] nodes show up in the Ltac profile

This closes #5082 and closes #5778, but makes #6404 apply to `abstract`
as well as `transparent_abstract`.  This is unfortunate, but I think it
is worth it to get `abstract` in the profile (and therefore not
misassign the time spent sending the subproof to the kernel).  Another
alternative would have been to add a dedicated entry to `ltac_call_kind`
for `TacAbstract`, but I think it's better to just deal with #6404 all
at once.

The "better" solution here would have been to move `abstract` out of the
Ltac syntax tree and define it via `TACTIC EXTEND` like
`transparent_abstract`.  However, the STM relies on its ability to
recognize `abstract` and `solve [ abstract ... ]` syntactically so that
it can handle `par: abstract`.

Note that had to add locations to `TacAbstract` nodes, as I could not
figure out how to call `push_trace` otherwise.

1 files changed, 7 insertions, 3 deletions

diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml
index ded902a8f..dccb7cb75 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 (loc,(t,ido)) ->
+      let call = LtacMLCall tac in
+      push_trace(loc,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 ->