From 52a71bf2b1260ce8f8622878c82caec54d298808 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Mon, 5 Apr 2021 16:24:39 +0200
Subject: Locations: Moving functions Ploc.sub and Ploc.after to loc.ml.

---
 gramlib/ploc.ml  |  5 -----
 gramlib/ploc.mli | 12 ------------
 2 files changed, 17 deletions(-)

(limited to 'gramlib')

diff --git a/gramlib/ploc.ml b/gramlib/ploc.ml
index e121342c94..44ba0c1f44 100644
--- a/gramlib/ploc.ml
+++ b/gramlib/ploc.ml
@@ -11,8 +11,3 @@ let make_unlined (bp, ep) =
 let dummy =
   {fname = InFile ""; line_nb = 1; bol_pos = 0; line_nb_last = -1; bol_pos_last = 0;
    bp = 0; ep = 0; }
-
-(* *)
-
-let sub loc sh len = {loc with bp = loc.bp + sh; ep = loc.bp + sh + len}
-let after loc sh len = {loc with bp = loc.ep + sh; ep = loc.ep + sh + len}
diff --git a/gramlib/ploc.mli b/gramlib/ploc.mli
index 4b865110c3..fad883e11a 100644
--- a/gramlib/ploc.mli
+++ b/gramlib/ploc.mli
@@ -9,15 +9,3 @@ val make_unlined : int * int -> Loc.t
 val dummy : Loc.t
    (** [Ploc.dummy] is a dummy location, used in situations when location
        has no meaning. *)
-
-(* combining locations *)
-
-val sub : Loc.t -> int -> int -> Loc.t
-   (** [Ploc.sub loc sh len] is the location [loc] shifted with [sh]
-       characters and with length [len]. The previous ending position
-       of the location is lost. *)
-
-val after : Loc.t -> int -> int -> Loc.t
-   (** [Ploc.after loc sh len] is the location just after loc (starting at
-       the end position of [loc]) shifted with [sh] characters and of length
-       [len]. *)
-- 
cgit v1.2.3