diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2018-04-12 11:10:28 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2018-04-12 11:10:28 +0200 |
| commit | 32b424902383a99436439a3c8ee24a528d1077a9 (patch) | |
| tree | dcf2c6e9e732d153f28e446e5ea748fa529329be /plugins/ltac | |
| parent | 8059a0efa79fcd72d56c424adf1bea10dae28d6d (diff) | |
| parent | df5c63872c2630d79b23c128ac47a62de3e9c322 (diff) | |
Merge PR #7107: Fixes #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 57a11d947..105b5c59a 100644 --- a/plugins/ltac/tactic_debug.ml +++ b/plugins/ltac/tactic_debug.ml @@ -399,8 +399,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 @@ -408,7 +406,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 *) @@ -417,7 +415,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 |