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.

6 files changed, 19 insertions, 15 deletions

diff --git a/plugins/ltac/g_ltac.ml4 b/plugins/ltac/g_ltac.ml4
index ebf6e450b..8dd4199e3 100644
--- a/plugins/ltac/g_ltac.ml4
+++ b/plugins/ltac/g_ltac.ml4
@@ -125,9 +125,9 @@ GEXTEND Gram
       | IDENT "exactly_once"; ta = tactic_expr -> TacExactlyOnce ta
       | IDENT "infoH"; ta = tactic_expr -> TacShowHyps ta
 (*To do: put Abstract in Refiner*)
-      | IDENT "abstract"; tc = NEXT -> TacAbstract (tc,None)
+      | IDENT "abstract"; tc = NEXT -> TacAbstract (Loc.tag ~loc:!@loc (tc,None))
       | IDENT "abstract"; tc = NEXT; "using";  s = ident ->
-          TacAbstract (tc,Some s)
+          TacAbstract (Loc.tag ~loc:!@loc (tc,Some s))
       | sel = selector; ta = tactic_expr -> TacSelect (sel, ta) ]
 (*End of To do*)
     | "2" RIGHTA
@@ -401,12 +401,12 @@ VERNAC ARGUMENT EXTEND ltac_use_default PRINTED BY pr_ltac_use_default
 END
 
 let is_anonymous_abstract = function
-  | TacAbstract (_,None) -> true
-  | TacSolve [TacAbstract (_,None)] -> true
+  | TacAbstract (_,(_,None)) -> true
+  | TacSolve [TacAbstract (_,(_,None))] -> true
   | _ -> false
 let rm_abstract = function
-  | TacAbstract (t,_) -> t
-  | TacSolve [TacAbstract (t,_)] -> TacSolve [t]
+  | TacAbstract (_,(t,_)) -> t
+  | TacSolve [TacAbstract (_,(t,_))] -> TacSolve [t]
   | x -> x
 let is_explicit_terminator = function TacSolve _ -> true | _ -> false
 
diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml
index e5ff47356..c9676ac6f 100644
--- a/plugins/ltac/pptactic.ml
+++ b/plugins/ltac/pptactic.ml
@@ -881,9 +881,9 @@ let pr_goal_selector ~toplevel s =
         let rec pr_tac inherited tac =
           let return (doc, l) = (tag tac doc, l) in
           let (strm, prec) = return (match tac with
-            | TacAbstract (t,None) ->
+            | TacAbstract (_,(t,None)) ->
               keyword "abstract " ++ pr_tac (labstract,L) t, labstract
-            | TacAbstract (t,Some s) ->
+            | TacAbstract (_,(t,Some s)) ->
               hov 0 (
                 keyword "abstract"
                 ++ str" (" ++ pr_tac (labstract,L) t ++ str")" ++ spc ()
diff --git a/plugins/ltac/tacexpr.mli b/plugins/ltac/tacexpr.mli
index ccd555b61..a98752e26 100644
--- a/plugins/ltac/tacexpr.mli
+++ b/plugins/ltac/tacexpr.mli
@@ -249,7 +249,7 @@ and 'a gen_tactic_expr =
   | TacProgress of 'a gen_tactic_expr
   | TacShowHyps of 'a gen_tactic_expr
   | TacAbstract of
-      'a gen_tactic_expr * Id.t option
+      ('a gen_tactic_expr * Id.t option) Loc.located
   | TacId of 'n message_token list
   | TacFail of global_flag * int or_var * 'n message_token list
   | TacInfo of 'a gen_tactic_expr
diff --git a/plugins/ltac/tacintern.ml b/plugins/ltac/tacintern.ml
index ebffde441..acdbc7d79 100644
--- a/plugins/ltac/tacintern.ml
+++ b/plugins/ltac/tacintern.ml
@@ -584,8 +584,8 @@ and intern_tactic_seq onlytac ist = function
       ist.ltacvars, TacFail (g,intern_int_or_var ist n,intern_message ist l)
   | TacProgress tac -> ist.ltacvars, TacProgress (intern_pure_tactic ist tac)
   | TacShowHyps tac -> ist.ltacvars, TacShowHyps (intern_pure_tactic ist tac)
-  | TacAbstract (tac,s) ->
-      ist.ltacvars, TacAbstract (intern_pure_tactic ist tac,s)
+  | TacAbstract (loc,(tac,s)) ->
+      ist.ltacvars, TacAbstract (loc,(intern_pure_tactic ist tac,s))
   | TacThen (t1,t2) ->
       let lfun', t1 = intern_tactic_seq onlytac ist t1 in
       let lfun'', t2 = intern_tactic_seq onlytac { ist with ltacvars = lfun' } t2 in
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 ->
diff --git a/plugins/ltac/tacsubst.ml b/plugins/ltac/tacsubst.ml
index 79bf3685e..2b4dd2a27 100644
--- a/plugins/ltac/tacsubst.ml
+++ b/plugins/ltac/tacsubst.ml
@@ -192,7 +192,7 @@ and subst_tactic subst (t:glob_tactic_expr) = match t with
   | TacId _ | TacFail _ as x -> x
   | TacProgress tac -> TacProgress (subst_tactic subst tac:glob_tactic_expr)
   | TacShowHyps tac -> TacShowHyps (subst_tactic subst tac:glob_tactic_expr)
-  | TacAbstract (tac,s) -> TacAbstract (subst_tactic subst tac,s)
+  | TacAbstract (loc,(tac,s)) -> TacAbstract (loc,(subst_tactic subst tac,s))
   | TacThen (t1,t2) ->
       TacThen (subst_tactic subst t1, subst_tactic subst t2)
   | TacDispatch tl -> TacDispatch (List.map (subst_tactic subst) tl)