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/dune | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to 'gramlib/dune')

diff --git a/gramlib/dune b/gramlib/dune
index 6a9e622b4c..8ca6aff25a 100644
--- a/gramlib/dune
+++ b/gramlib/dune
@@ -1,3 +1,4 @@
 (library
  (name gramlib)
- (public_name coq.gramlib))
+ (public_name coq.gramlib)
+ (libraries coq.lib))
-- 
cgit v1.2.3