From a4458475187de726b1518e536cb1a42e8c9d0534 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sat, 29 Oct 2016 01:18:30 +0200
Subject: Fixing #5164 (regression in locating error in argument of "refine").

Reporting location was not expecting a term passed to an ML tactic to
be interpreted by the ML tactic itself. Made an empirical fix to
report about the as-precise-as-possible location available.
---
 ltac/tactic_debug.ml | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

diff --git a/ltac/tactic_debug.ml b/ltac/tactic_debug.ml
index e1c9fed637..5cbddc7f64 100644
--- a/ltac/tactic_debug.ml
+++ b/ltac/tactic_debug.ml
@@ -385,6 +385,8 @@ let skip_extensions trace =
   | [] -> [] in
   List.rev (aux (List.rev trace))
 
+let finer_loc loc1 loc2 = Loc.merge loc1 loc2 = loc2
+
 let extract_ltac_trace trace eloc =
   let trace = skip_extensions trace in
   let (loc,c),tail = List.sep_last trace in
@@ -392,11 +394,10 @@ let extract_ltac_trace trace eloc =
     (* We entered a user-defined tactic,
        we display the trace with location of the call *)
     let msg = hov 0 (explain_ltac_call_trace c tail eloc ++ fnl()) in
-    Some msg, loc
+    Some msg, if finer_loc eloc loc then eloc else loc
   else
     (* We entered a primitive tactic, we don't display trace but
        report on the finest location *)
-    let finer_loc loc1 loc2 = Loc.merge loc1 loc2 = loc2 in
     let best_loc =
       (* trace is with innermost call coming first *)
       let rec aux best_loc = function
-- 
cgit v1.2.3