From df5c63872c2630d79b23c128ac47a62de3e9c322 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Wed, 28 Mar 2018 22:07:26 +0200
Subject: Fixing #7100 (lost of main file location in case of Ltac failure in
 other file).

---
 plugins/ltac/tactic_debug.ml | 6 ++----
 1 file changed, 2 insertions(+), 4 deletions(-)

(limited to 'plugins/ltac/tactic_debug.ml')

diff --git a/plugins/ltac/tactic_debug.ml b/plugins/ltac/tactic_debug.ml
index e55b49fb4e..bb815dcb3f 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
-- 
cgit v1.2.3