7 files changed, 41 insertions, 9 deletions
diff --git a/doc/changelog/05-tactic-language/13247-master+fix13241-locating-nested-ltac-errors.rst b/doc/changelog/05-tactic-language/13247-master+fix13241-locating-nested-ltac-errors.rst
new file mode 100644
index 0000000000..1eb8ef5a2a
--- /dev/null
+++ b/doc/changelog/05-tactic-language/13247-master+fix13241-locating-nested-ltac-errors.rst
@@ -0,0 +1,6 @@
+- **Fixed:**
+  Miscellaneous issues with locating tactic errors
+  (`#13247 <https://github.com/coq/coq/pull/13247>`_,
+  fixes `#12773 <https://github.com/coq/coq/issues/12773>`_
+  and `#12992 <https://github.com/coq/coq/issues/12992>`_,
+  by Hugo Herbelin).
diff --git a/plugins/ltac/taccoerce.ml b/plugins/ltac/taccoerce.ml
index ee28229cb7..4c1fe6417e 100644
--- a/plugins/ltac/taccoerce.ml
+++ b/plugins/ltac/taccoerce.ml
@@ -394,8 +394,13 @@ type appl =
 
 (* Values for interpretation *)
 type tacvalue =
-  | VFun of appl * Tacexpr.ltac_trace * Loc.t option * Val.t Id.Map.t *
-      Name.t list * Tacexpr.glob_tactic_expr
+  | VFun of
+      appl *
+      Tacexpr.ltac_trace *
+      Loc.t option * (* when executing a global Ltac function: the location where this function was called *)
+      Val.t Id.Map.t * (* closure *)
+      Name.t list * (* binders *)
+      Tacexpr.glob_tactic_expr (* body *)
   | VRec of Val.t Id.Map.t ref * Tacexpr.glob_tactic_expr
 
 let (wit_tacvalue : (Empty.t, tacvalue, tacvalue) Genarg.genarg_type) =
diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml
index 7728415ddd..3d734d3a66 100644
--- a/plugins/ltac/tacinterp.ml
+++ b/plugins/ltac/tacinterp.ml
@@ -153,11 +153,15 @@ let add_extra_loc loc extra =
   match loc with
   | None -> extra
   | Some loc -> TacStore.set extra f_loc loc
-let add_loc loc ist =
+let extract_loc ist = TacStore.get ist.extra f_loc
+
+let ensure_loc loc ist =
   match loc with
   | None -> ist
-  | Some loc -> { ist with extra = TacStore.set ist.extra f_loc loc }
-let extract_loc ist = TacStore.get ist.extra f_loc
+  | Some loc ->
+    match extract_loc ist with
+    | None -> { ist with extra = TacStore.set ist.extra f_loc loc }
+    | Some _ -> ist
 
 let print_top_val env v = Pptactic.pr_value Pptactic.ltop v
 
@@ -1175,7 +1179,7 @@ and eval_tactic_ist ist tac : unit Proofview.tactic = match tac with
   | TacFirst l -> Tacticals.New.tclFIRST (List.map (interp_tactic ist) l)
   | TacSolve l -> Tacticals.New.tclSOLVE (List.map (interp_tactic ist) l)
   | TacComplete tac -> Tacticals.New.tclCOMPLETE (interp_tactic ist tac)
-  | TacArg {CAst.loc} -> Ftactic.run (val_interp (add_loc loc ist) tac) (fun v -> tactic_of_value ist v)
+  | TacArg {CAst.loc} -> Ftactic.run (val_interp (ensure_loc loc ist) tac) (fun v -> tactic_of_value ist v)
   | TacSelect (sel, tac) -> Tacticals.New.tclSELECT sel (interp_tactic ist tac)
   (* For extensions *)
   | TacAlias {loc; v=(s,l)} ->
@@ -1254,9 +1258,12 @@ and interp_ltac_reference ?loc' mustbetac ist r : Val.t Ftactic.t =
       let extra = TacStore.set extra f_trace trace in
       let ist = { lfun = Id.Map.empty; poly; extra } in
       let appl = GlbAppl[r,[]] in
+      (* We call a global ltac reference: add a loc on its executation only if not
+         already in another global reference *)
+      let ist = ensure_loc loc ist in
       Profile_ltac.do_profile "interp_ltac_reference" trace ~count_call:false
-        (catch_error_tac_loc (* interp *) loc false trace
-           (val_interp ~appl (add_loc (* exec *) loc ist) (Tacenv.interp_ltac r)))
+        (catch_error_tac_loc (* loc for interpretation *) loc false trace
+           (val_interp ~appl ist (Tacenv.interp_ltac r)))
 
 and interp_tacarg ist arg : Val.t Ftactic.t =
   match arg with
@@ -1325,7 +1332,7 @@ and interp_app loc ist fv largs : Val.t Ftactic.t =
                 ; extra = TacStore.set ist.extra f_trace []
                 } in
               Profile_ltac.do_profile "interp_app" trace ~count_call:false
-                (catch_error_tac_loc loc false trace (val_interp (add_loc loc ist) body)) >>= fun v ->
+                (catch_error_tac_loc loc false trace (val_interp (ensure_loc loc ist) body)) >>= fun v ->
               Ftactic.return (name_vfun (push_appl appl largs) v)
             end
             begin fun (e, info) ->
diff --git a/test-suite/output/ErrorLocation_13241_1.out b/test-suite/output/ErrorLocation_13241_1.out
new file mode 100644
index 0000000000..d899dd5d46
--- /dev/null
+++ b/test-suite/output/ErrorLocation_13241_1.out
@@ -0,0 +1,3 @@
+File "stdin", line 4, characters 0-1:
+Error: No product even after head-reduction.
+
diff --git a/test-suite/output/ErrorLocation_13241_1.v b/test-suite/output/ErrorLocation_13241_1.v
new file mode 100644
index 0000000000..ff92085133
--- /dev/null
+++ b/test-suite/output/ErrorLocation_13241_1.v
@@ -0,0 +1,4 @@
+Ltac a := intro.
+Ltac b := a.
+Goal True.
+b.
diff --git a/test-suite/output/ErrorLocation_13241_2.out b/test-suite/output/ErrorLocation_13241_2.out
new file mode 100644
index 0000000000..d899dd5d46
--- /dev/null
+++ b/test-suite/output/ErrorLocation_13241_2.out
@@ -0,0 +1,3 @@
+File "stdin", line 4, characters 0-1:
+Error: No product even after head-reduction.
+
diff --git a/test-suite/output/ErrorLocation_13241_2.v b/test-suite/output/ErrorLocation_13241_2.v
new file mode 100644
index 0000000000..280d4a3506
--- /dev/null
+++ b/test-suite/output/ErrorLocation_13241_2.v
@@ -0,0 +1,4 @@
+Ltac a _ := intro.
+Ltac b := a ().
+Goal True.
+b.