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`
---
 dev/ci/user-overlays/09065-ejgallego-gramlib+no_ploc.sh | 6 ++++++
 1 file changed, 6 insertions(+)
 create mode 100644 dev/ci/user-overlays/09065-ejgallego-gramlib+no_ploc.sh

(limited to 'dev')

diff --git a/dev/ci/user-overlays/09065-ejgallego-gramlib+no_ploc.sh b/dev/ci/user-overlays/09065-ejgallego-gramlib+no_ploc.sh
new file mode 100644
index 0000000000..e9daa7a44e
--- /dev/null
+++ b/dev/ci/user-overlays/09065-ejgallego-gramlib+no_ploc.sh
@@ -0,0 +1,6 @@
+if [ "$CI_PULL_REQUEST" = "9065" ] || [ "$CI_BRANCH" = "gramlib+no_ploc" ]; then
+
+    elpi_CI_REF=gramlib+no_ploc
+    elpi_CI_GITURL=https://github.com/ejgallego/coq-elpi
+
+fi
-- 
cgit v1.2.3