From c064fb933a16dc25b8172a1a2e758f538ee7285e Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sat, 18 Jun 2016 11:18:01 +0200
Subject: A hack to fix another regression with Ltac trace report in 8.5. E.g.

Goal 0=0 -> true=true.
intro H; rewrite H1.

was highlighting H1 but

Goal 0=0 -> true=true.
intro H; rewrite H.

was only highlighting the whole "intro H; rewrite H".
---
 toplevel/himsg.ml | 19 ++++++++++++-------
 1 file changed, 12 insertions(+), 7 deletions(-)

diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml
index 244174f651..13a6489b9d 100644
--- a/toplevel/himsg.ml
+++ b/toplevel/himsg.ml
@@ -1307,12 +1307,17 @@ let extract_ltac_trace trace eloc =
   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 =
-      if not (Loc.is_ghost eloc) then eloc else
-        (* trace is with innermost call coming first *)
-        let rec aux = function
-        | (loc,_)::tail when not (Loc.is_ghost loc) -> loc
-        | _::tail -> aux tail
-        | [] -> Loc.ghost in
-        aux trace in
+      (* trace is with innermost call coming first *)
+      let rec aux best_loc = function
+        | (loc,_)::tail ->
+           if Loc.is_ghost best_loc ||
+              not (Loc.is_ghost loc) && finer_loc loc best_loc
+           then
+             aux loc tail
+           else
+             aux best_loc tail
+        | [] -> best_loc in
+        aux eloc trace in
     None, best_loc
-- 
cgit v1.2.3