diff options
| author |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-01-18 15:46:23 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-04-25 00:28:53 +0200 |
| commit | e8a6467545c2814c9418889201e8be19c0cef201 (patch) | |
| tree | 7f513d854b76b02f52f98ee0e87052c376175a0f /plugins/ltac/tactic_debug.ml | |
| parent | 30d3515546cf244837c6340b6b87c5f51e68cbf4 (diff) | |
[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.
Diffstat (limited to 'plugins/ltac/tactic_debug.ml')
| -rw-r--r-- | plugins/ltac/tactic_debug.ml | 7 |
1 files changed, 3 insertions, 4 deletions
diff --git a/plugins/ltac/tactic_debug.ml b/plugins/ltac/tactic_debug.ml index ac8534bdc..f04495c61 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 |