diff options
| -rw-r--r-- | interp/dumpglob.ml | 7 | ||||
| -rw-r--r-- | lib/loc.ml | 2 |
2 files changed, 6 insertions, 3 deletions
diff --git a/interp/dumpglob.ml b/interp/dumpglob.ml index c18ceecab..c7d3da653 100644 --- a/interp/dumpglob.ml +++ b/interp/dumpglob.ml @@ -139,12 +139,15 @@ let interval loc = loc1, loc2-1 let dump_ref loc filepath modpath ident ty = - if !glob_output = Feedback then + match !glob_output with + | Feedback -> Pp.feedback (Feedback.GlobRef (loc, filepath, modpath, ident, ty)) - else + | NoGlob -> () + | _ when not (Loc.is_ghost loc) -> let bl,el = interval loc in dump_string (Printf.sprintf "R%d:%d %s %s %s %s\n" bl el filepath modpath ident ty) + | _ -> () let dump_reference loc modpath ident ty = let filepath = Names.DirPath.to_string (Lib.library_dp ()) in diff --git a/lib/loc.ml b/lib/loc.ml index b62677d48..9043bee07 100644 --- a/lib/loc.ml +++ b/lib/loc.ml @@ -31,7 +31,7 @@ let ghost = { fname = ""; line_nb = -1; bol_pos = 0; line_nb_last = -1; bol_pos_last = 0; bp = 0; ep = 0; } -let is_ghost loc = Pervasives.(=) loc ghost (** FIXME *) +let is_ghost loc = loc.ep = 0 let merge loc1 loc2 = if loc1.bp < loc2.bp then |