aboutsummaryrefslogtreecommitdiffhomepage
path: root/lib/loc.ml
diff options
context:
space:
mode:
Diffstat (limited to 'lib/loc.ml')
-rw-r--r--lib/loc.ml4
1 files changed, 0 insertions, 4 deletions
diff --git a/lib/loc.ml b/lib/loc.ml
index e02fe108d..9107dce47 100644
--- a/lib/loc.ml
+++ b/lib/loc.ml
@@ -55,10 +55,6 @@ let unloc loc = (loc.bp, loc.ep)
let join_loc = merge
-let internal_ghost = {
- fname = ""; line_nb = -1; bol_pos = 0; line_nb_last = -1; bol_pos_last = 0;
- bp = 0; ep = 0; }
-
(** Located type *)
type 'a located = t option * 'a