From 0422f7e67c6c87ab364212a267288afcc7313e90 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Sat, 24 Nov 2018 21:41:22 +0100
Subject: [gramlib] Remove `Ploc.t` in favor of `Loc.t`

The types are identical and we have no more reason for the split. Note
the following TODOS:

- discrepancy of `Ploc.after` with `CLexer.after`
- discrepancy of `Ploc.comments` with `CLexer.comments`
- `Ploc.dummy` vs `Loc.t option`
---
 gramlib/plexing.ml | 5 ++---
 1 file changed, 2 insertions(+), 3 deletions(-)

(limited to 'gramlib/plexing.ml')

diff --git a/gramlib/plexing.ml b/gramlib/plexing.ml
index 986363ec1f..7b8618fd20 100644
--- a/gramlib/plexing.ml
+++ b/gramlib/plexing.ml
@@ -6,8 +6,7 @@ type pattern = string * string
 
 exception Error of string
 
-type location = Ploc.t
-type location_function = int -> location
+type location_function = int -> Loc.t
 type 'te lexer_func = char Stream.t -> 'te Stream.t * location_function
 
 type 'te lexer =
@@ -16,4 +15,4 @@ type 'te lexer =
     tok_removing : pattern -> unit;
     mutable tok_match : pattern -> 'te -> string;
     tok_text : pattern -> string;
-    mutable tok_comm : location list option }
+    mutable tok_comm : Loc.t list option }
-- 
cgit v1.2.3