From af7628468d638c77fb3f55a9eb315b687b76a21d Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Fri, 21 Feb 2020 12:20:00 -0500
Subject: [parsing] Remove redundant interfaces from Pcoq

There is not need to re-export Gramlib's API in a non-structured way
anymore. We thus expose the core Gramlib interface to users and remove
redundant functions.

A question about whether to move more parts of the API to `Gramlib` is
still open, as well as on naming.
---
 plugins/ltac/g_tactic.mlg | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'plugins/ltac')

diff --git a/plugins/ltac/g_tactic.mlg b/plugins/ltac/g_tactic.mlg
index 5a26ac8827..bec83411c1 100644
--- a/plugins/ltac/g_tactic.mlg
+++ b/plugins/ltac/g_tactic.mlg
@@ -62,7 +62,7 @@ open Extraargs
 
 (* idem for (x1..xn:t) [n^2 complexity but exceptional use] *)
 let check_for_coloneq =
-  Pcoq.Entry.of_parser "lpar_id_colon"
+  Pcoq.G.Entry.of_parser "lpar_id_colon"
     (fun _ strm ->
       let rec skip_to_rpar p n =
         match List.last (Stream.npeek n strm) with
-- 
cgit v1.2.3