From e8a6467545c2814c9418889201e8be19c0cef201 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Wed, 18 Jan 2017 15:46:23 +0100
Subject: [location] Make location optional in Loc.located

This completes the Loc.ghost removal, the idea is to gear the API
towards optional, but uniform, location handling.

We don't print <unknown> anymore in the case there is no location.
This is what the test suite expects.

The old printing logic for located items was a bit inconsistent as
it sometimes printed <unknown> and other times it printed nothing as
the caller checked for `is_ghost` upstream.
---
 plugins/ltac/tactic_debug.ml | 7 +++----
 1 file changed, 3 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 ac8534bdc4..f04495c61d 100644
--- a/plugins/ltac/tactic_debug.ml
+++ b/plugins/ltac/tactic_debug.ml
@@ -387,12 +387,11 @@ let skip_extensions trace =
   | [] -> [] in
   List.rev (aux (List.rev trace))
 
-let finer_loc loc1 loc2 = Loc.merge loc1 loc2 = loc2
+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
-  let loc = Option.default tloc loc       in
   if is_defined_ltac trace then
     (* We entered a user-defined tactic,
        we display the trace with location of the call *)
@@ -405,8 +404,8 @@ let extract_ltac_trace ?loc trace =
       (* 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
+           if Option.is_empty best_loc ||
+              not (Option.is_empty loc) && finer_loc loc best_loc
            then
              aux loc tail
            else
-- 
cgit v1.2.3