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.

2 files changed, 11 insertions, 0 deletions

diff --git a/test-suite/output/bug5778.out b/test-suite/output/bug5778.out
new file mode 100644
index 000000000..91ceb1b58
--- /dev/null
+++ b/test-suite/output/bug5778.out
@@ -0,0 +1,4 @@
+The command has indeed failed with message:
+In nested Ltac calls to "c", "abs" and "abstract b ltac:(())", last call
+failed.
+The term "I" has type "True" which should be Set, Prop or Type.
diff --git a/test-suite/output/bug5778.v b/test-suite/output/bug5778.v
new file mode 100644
index 000000000..0dcd76aef
--- /dev/null
+++ b/test-suite/output/bug5778.v
@@ -0,0 +1,7 @@
+Ltac a _ := pose (I : I).
+Ltac b _ := a ().
+Ltac abs _ := abstract b ().
+Ltac c _ := abs ().
+Goal True.
+  Fail c ().
+Abort.