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.

0 files changed, 0 insertions, 0 deletions