4 files changed, 11 insertions, 4 deletions

diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml
index e7ee5a594f..2ca9a0e69d 100644
--- a/plugins/ltac/tacinterp.ml
+++ b/plugins/ltac/tacinterp.ml
@@ -182,7 +182,7 @@ let catch_error_with_trace_loc loc use_finer call_trace f x =
     catching_error call_trace Exninfo.iraise e
 
 let catch_error_loc loc use_finer tac =
-  Proofview.tclOR tac (fun exn ->
+  Proofview.tclORELSE tac (fun exn ->
       let (e, info) = update_loc loc use_finer exn in
       Proofview.tclZERO ~info e)
 
@@ -1163,7 +1163,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 a -> interp_tactic ist (TacArg a)
+  | TacArg a -> Ftactic.run (val_interp ist tac) (fun v -> catch_error_loc a.CAst.loc false (tactic_of_value ist v))
   | TacSelect (sel, tac) -> Tacticals.New.tclSELECT sel (interp_tactic ist tac)
   (* For extensions *)
   | TacAlias {loc; v=(s,l)} ->
@@ -1243,7 +1243,7 @@ and interp_ltac_reference ?loc' mustbetac ist r : Val.t Ftactic.t =
       let ist = { lfun = Id.Map.empty; poly; extra } in
       let appl = GlbAppl[r,[]] in
       Profile_ltac.do_profile "interp_ltac_reference" trace ~count_call:false
-        (val_interp ~appl ist (Tacenv.interp_ltac r))
+        (catch_error_tac_loc loc false trace (val_interp ~appl ist (Tacenv.interp_ltac r)))
 
 and interp_tacarg ist arg : Val.t Ftactic.t =
   match arg with
diff --git a/test-suite/output/ErrorLocation_12774_3.out b/test-suite/output/ErrorLocation_12774_3.out
new file mode 100644
index 0000000000..dbd3dbd1e2
--- /dev/null
+++ b/test-suite/output/ErrorLocation_12774_3.out
@@ -0,0 +1,3 @@
+File "stdin", line 3, characters 0-1:
+Error: No product even after head-reduction.
+
diff --git a/test-suite/output/ErrorLocation_12774_3.v b/test-suite/output/ErrorLocation_12774_3.v
new file mode 100644
index 0000000000..c624402a81
--- /dev/null
+++ b/test-suite/output/ErrorLocation_12774_3.v
@@ -0,0 +1,4 @@
+Ltac f := auto; intro.
+Goal False.
+f.
+Abort.
diff --git a/test-suite/output/Error_msg_diffs.out b/test-suite/output/Error_msg_diffs.out
index 3e337e892d..2645524a70 100644
--- a/test-suite/output/Error_msg_diffs.out
+++ b/test-suite/output/Error_msg_diffs.out
@@ -1,4 +1,4 @@
-File "stdin", line 32, characters 0-12:
+File "stdin", line 32, characters 0-11:
 Error:
 In environment
 T : Type