Pass a ghost location for abstract

As per request at https://github.com/coq/coq/pull/6406#pullrequestreview-83503902

6 files changed, 14 insertions, 14 deletions

diff --git a/plugins/ltac/g_ltac.ml4 b/plugins/ltac/g_ltac.ml4
index 8dd4199e3..ebf6e450b 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 (Loc.tag ~loc:!@loc (tc,None))
+      | IDENT "abstract"; tc = NEXT -> TacAbstract (tc,None)
       | IDENT "abstract"; tc = NEXT; "using";  s = ident ->
-          TacAbstract (Loc.tag ~loc:!@loc (tc,Some s))
+          TacAbstract (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 c9676ac6f..e5ff47356 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 a98752e26..ccd555b61 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) Loc.located
+      'a gen_tactic_expr * Id.t option
   | 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 acdbc7d79..ebffde441 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 (loc,(tac,s)) ->
-      ist.ltacvars, TacAbstract (loc,(intern_pure_tactic ist tac,s))
+  | TacAbstract (tac,s) ->
+      ist.ltacvars, TacAbstract (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 dccb7cb75..73c0874d2 100644
--- a/plugins/ltac/tacinterp.ml
+++ b/plugins/ltac/tacinterp.ml
@@ -1158,9 +1158,9 @@ 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 (loc,(t,ido)) ->
+  | TacAbstract (t,ido) ->
       let call = LtacMLCall tac in
-      push_trace(loc,call) ist >>= fun trace ->
+      push_trace(None,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
diff --git a/plugins/ltac/tacsubst.ml b/plugins/ltac/tacsubst.ml
index 2b4dd2a27..79bf3685e 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 (loc,(tac,s)) -> TacAbstract (loc,(subst_tactic subst tac,s))
+  | TacAbstract (tac,s) -> TacAbstract (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)