diff options
author | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2016-06-18 11:18:01 +0200 |
---|---|---|
committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2016-06-18 11:18:01 +0200 |
commit | c064fb933a16dc25b8172a1a2e758f538ee7285e (patch) | |
tree | 1dcb78fe37b19a4d063a1ef2ba7bfba2135e40bc /toplevel/himsg.ml | |
parent | 5401deb474ca596ffbb23a12f4b70e6def1d0d65 (diff) |
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".
Diffstat (limited to 'toplevel/himsg.ml')
-rw-r--r-- | toplevel/himsg.ml | 19 |
1 files changed, 12 insertions, 7 deletions
diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml index 244174f65..13a6489b9 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 |