diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2018-03-28 22:07:26 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2018-04-04 17:18:22 +0200 |
| commit | df5c63872c2630d79b23c128ac47a62de3e9c322 (patch) | |
| tree | cd47fd6d454164a2e8cf34886a0ed22d3acc0ac3 /plugins/ltac | |
| parent | e128900aee63c972d7977fd47e3fd21649b63409 (diff) | |
Fixing #7100 (lost of main file location in case of Ltac failure in other file).
Diffstat (limited to 'plugins/ltac')
| -rw-r--r-- | plugins/ltac/tactic_debug.ml | 6 |
1 files changed, 2 insertions, 4 deletions
diff --git a/plugins/ltac/tactic_debug.ml b/plugins/ltac/tactic_debug.ml index e55b49fb4..bb815dcb3 100644 --- a/plugins/ltac/tactic_debug.ml +++ b/plugins/ltac/tactic_debug.ml @@ -402,8 +402,6 @@ let skip_extensions trace = | [] -> [] in List.rev (aux (List.rev trace)) -let finer_loc loc1 loc2 = Loc.merge_opt loc1 loc2 = loc2 - let extract_ltac_trace ?loc trace = let trace = skip_extensions trace in let (tloc,c),tail = List.sep_last trace in @@ -411,7 +409,7 @@ let extract_ltac_trace ?loc trace = (* 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 loc ++ fnl()) in - (if finer_loc loc tloc then loc else tloc), Some msg + (if Loc.finer loc tloc then loc else tloc), Some msg else (* We entered a primitive tactic, we don't display trace but report on the finest location *) @@ -420,7 +418,7 @@ let extract_ltac_trace ?loc trace = let rec aux best_loc = function | (loc,_)::tail -> if Option.is_empty best_loc || - not (Option.is_empty loc) && finer_loc loc best_loc + not (Option.is_empty loc) && Loc.finer loc best_loc then aux loc tail else |