diff options
| author | Hugo Herbelin | 2016-06-18 11:23:12 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2016-06-18 13:09:16 +0200 |
| commit | 7ee82cd2dfd8cb226c35c3094423e56c75010377 (patch) | |
| tree | 7a681820b8a475da703e025cc2e4a0182887604d /ltac | |
| parent | f841c27c1cfd38aada72f3c8f90e2ed1ec22db6a (diff) | |
Backporting c064fb933 from 8.5 (another regression with Ltac trace report).
Doing it explicitly because it is in another file.
Diffstat (limited to 'ltac')
| -rw-r--r-- | ltac/tactic_debug.ml | 19 |
1 files changed, 12 insertions, 7 deletions
diff --git a/ltac/tactic_debug.ml b/ltac/tactic_debug.ml index e657eb9bc2..73d04b810d 100644 --- a/ltac/tactic_debug.ml +++ b/ltac/tactic_debug.ml @@ -395,14 +395,19 @@ 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 let get_ltac_trace (_, info) = |