9 files changed, 62 insertions, 15 deletions
diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml
index fdebe14a23..3228c6afd4 100644
--- a/plugins/ltac/tacinterp.ml
+++ b/plugins/ltac/tacinterp.ml
@@ -161,27 +161,45 @@ let catching_error call_trace fail (e, info) =
     fail located_exc
   end
 
-let update_loc ?loc (e, info) =
-  (e, Option.cata (Loc.add_loc info) info loc)
+let update_loc loc use_finer (e, info as e') =
+  match loc with
+  | Some loc ->
+    if use_finer then
+      (* ensure loc if there is none *)
+      match Loc.get_loc info with
+      | None -> (e, Loc.add_loc info loc)
+      | _ -> (e, info)
+    else
+      (* override loc (because loc refers to inside of Ltac functions) *)
+      (e, Loc.add_loc info loc)
+  | None -> e'
 
-let catch_error ?loc call_trace f x =
+let catch_error_with_trace_loc loc use_finer call_trace f x =
   try f x
   with e when CErrors.noncritical e ->
     let e = Exninfo.capture e in
-    let e = update_loc ?loc e in
+    let e = update_loc loc use_finer e in
     catching_error call_trace Exninfo.iraise e
 
-let catch_error_loc ?loc tac =
+let catch_error_loc loc use_finer tac =
   Proofview.tclOR tac (fun exn ->
-      let (e, info) = update_loc ?loc exn in
+      let (e, info) = update_loc loc use_finer exn in
       Proofview.tclZERO ~info e)
 
-let wrap_error ?loc tac k =
+let wrap_error tac k =
+  if is_traced () then Proofview.tclORELSE tac k else tac
+
+let wrap_error_loc loc use_finer tac k =
   if is_traced () then Proofview.tclORELSE tac k
-  else catch_error_loc ?loc tac
+  else catch_error_loc loc use_finer tac
+
+let catch_error_tac call_trace tac =
+  wrap_error
+    tac
+    (catching_error call_trace (fun (e, info) -> Proofview.tclZERO ~info e))
 
-let catch_error_tac ?loc call_trace tac =
-  wrap_error ?loc
+let catch_error_tac_loc loc use_finer call_trace tac =
+  wrap_error_loc loc use_finer
     tac
     (catching_error call_trace (fun (e, info) -> Proofview.tclZERO ~info e))
 
@@ -553,7 +571,7 @@ let interp_gen kind ist pattern_mode flags env sigma c =
   let loc = loc_of_glob_constr term in
   let trace = push_trace (loc,LtacConstrInterp (term,vars)) ist in
   let (evd,c) =
-    catch_error ?loc trace (understand_ltac flags env sigma vars kind) term
+    catch_error_with_trace_loc loc true trace (understand_ltac flags env sigma vars kind) term
   in
   (* spiwack: to avoid unnecessary modifications of tacinterp, as this
      function already use effect, I call [run] hoping it doesn't mess
@@ -1071,7 +1089,7 @@ and eval_tactic ist tac : unit Proofview.tactic = match tac with
       let call = LtacAtomCall t in
       let trace = push_trace(loc,call) ist in
       Profile_ltac.do_profile "eval_tactic:2" trace
-        (catch_error_tac ?loc trace (interp_atomic ist t))
+        (catch_error_tac_loc loc true trace (interp_atomic ist t))
   | TacFun _ | TacLetIn _ | TacMatchGoal _ | TacMatch _ -> interp_tactic ist tac
   | TacId [] -> Proofview.tclLIFT (db_breakpoint (curr_debug ist) [])
   | TacId s ->
@@ -1162,7 +1180,7 @@ and eval_tactic ist tac : unit Proofview.tactic = match tac with
         ; poly
         ; extra = TacStore.set ist.extra f_trace trace } in
         val_interp ist alias.Tacenv.alias_body >>= fun v ->
-        Ftactic.lift (catch_error_loc ?loc (tactic_of_value ist v))
+        Ftactic.lift (catch_error_loc loc false (tactic_of_value ist v))
       in
       let tac =
         Ftactic.with_env interp_vars >>= fun (env, lr) ->
@@ -1191,7 +1209,7 @@ and eval_tactic ist tac : unit Proofview.tactic = match tac with
       let args = Ftactic.List.map_right (fun a -> interp_tacarg ist a) l in
       let tac args =
         let name _ _ = Pptactic.pr_extend (fun v -> print_top_val () v) 0 opn args in
-        Proofview.Trace.name_tactic name (catch_error_tac ?loc trace (tac args ist))
+        Proofview.Trace.name_tactic name (catch_error_tac_loc loc false trace (tac args ist))
       in
       Ftactic.run args tac
 
@@ -1294,7 +1312,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 trace (val_interp ist body)) >>= fun v ->
+                (catch_error_tac_loc loc false trace (val_interp 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_12774_1.out b/test-suite/output/ErrorLocation_12774_1.out
new file mode 100644
index 0000000000..e27992ed59
--- /dev/null
+++ b/test-suite/output/ErrorLocation_12774_1.out
@@ -0,0 +1,3 @@
+File "stdin", line 2, characters 13-14:
+Error: The term "0" has type "nat" while it is expected to have type "Type".
+
diff --git a/test-suite/output/ErrorLocation_12774_1.v b/test-suite/output/ErrorLocation_12774_1.v
new file mode 100644
index 0000000000..8516d402d1
--- /dev/null
+++ b/test-suite/output/ErrorLocation_12774_1.v
@@ -0,0 +1,3 @@
+Goal Type.
+simpl; exact 0.
+Abort.
diff --git a/test-suite/output/ErrorLocation_12774_2.out b/test-suite/output/ErrorLocation_12774_2.out
new file mode 100644
index 0000000000..434275eca5
--- /dev/null
+++ b/test-suite/output/ErrorLocation_12774_2.out
@@ -0,0 +1,3 @@
+File "stdin", line 3, characters 9-10:
+Error: The term "0" has type "nat" while it is expected to have type "Type".
+
diff --git a/test-suite/output/ErrorLocation_12774_2.v b/test-suite/output/ErrorLocation_12774_2.v
new file mode 100644
index 0000000000..e50e1caa0f
--- /dev/null
+++ b/test-suite/output/ErrorLocation_12774_2.v
@@ -0,0 +1,4 @@
+Ltac f := simpl.
+Goal Type.
+f; exact 0.
+Abort.
diff --git a/test-suite/output/ErrorLocation_tac_in_term_1.out b/test-suite/output/ErrorLocation_tac_in_term_1.out
new file mode 100644
index 0000000000..55ad5a36da
--- /dev/null
+++ b/test-suite/output/ErrorLocation_tac_in_term_1.out
@@ -0,0 +1,4 @@
+File "stdin", line 2, characters 21-25:
+Error:
+The term "true" has type "bool" while it is expected to have type "nat".
+
diff --git a/test-suite/output/ErrorLocation_tac_in_term_1.v b/test-suite/output/ErrorLocation_tac_in_term_1.v
new file mode 100644
index 0000000000..ef0b5aa757
--- /dev/null
+++ b/test-suite/output/ErrorLocation_tac_in_term_1.v
@@ -0,0 +1,3 @@
+Goal True.
+apply ltac:(apply (S true)).
+Abort.
diff --git a/test-suite/output/ErrorLocation_tac_in_term_2.out b/test-suite/output/ErrorLocation_tac_in_term_2.out
new file mode 100644
index 0000000000..5bff5ede43
--- /dev/null
+++ b/test-suite/output/ErrorLocation_tac_in_term_2.out
@@ -0,0 +1,4 @@
+File "stdin", line 4, characters 12-20:
+Error:
+The term "true" has type "bool" while it is expected to have type "nat".
+
diff --git a/test-suite/output/ErrorLocation_tac_in_term_2.v b/test-suite/output/ErrorLocation_tac_in_term_2.v
new file mode 100644
index 0000000000..e0fc2a9f4f
--- /dev/null
+++ b/test-suite/output/ErrorLocation_tac_in_term_2.v
@@ -0,0 +1,5 @@
+Ltac f x y := apply (x y).
+
+Goal True.
+apply ltac:(f S true).
+Abort.