[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.

3 files changed, 8 insertions, 8 deletions

diff --git a/toplevel/coqloop.ml b/toplevel/coqloop.ml
index b8acdd3af1..0d9edb248b 100644
--- a/toplevel/coqloop.ml
+++ b/toplevel/coqloop.ml
@@ -23,7 +23,7 @@ type input_buffer = {
   mutable str : Bytes.t; (* buffer of already read characters *)
   mutable len : int;    (* number of chars in the buffer *)
   mutable bols : int list; (* offsets in str of beginning of lines *)
-  mutable tokens : Pcoq.Parsable.t; (* stream of tokens *)
+  mutable tokens : Pcoq.G.Parsable.t; (* stream of tokens *)
   mutable start : int } (* stream count of the first char of the buffer *)
 
 (* Double the size of the buffer. *)
@@ -76,7 +76,7 @@ let reset_input_buffer doc ic ibuf =
   ibuf.str <- Bytes.empty;
   ibuf.len <- 0;
   ibuf.bols <- [];
-  ibuf.tokens <- Pcoq.Parsable.make (Stream.from (prompt_char doc ic ibuf));
+  ibuf.tokens <- Pcoq.G.Parsable.make (Stream.from (prompt_char doc ic ibuf));
   ibuf.start <- 0
 
 (* Functions to print underlined locations from an input buffer. *)
@@ -230,7 +230,7 @@ let top_buffer =
     str = Bytes.empty;
     len = 0;
     bols = [];
-    tokens = Pcoq.Parsable.make (Stream.of_list []);
+    tokens = Pcoq.G.Parsable.make (Stream.of_list []);
     start = 0 }
 
 let set_prompt prompt =
@@ -247,7 +247,7 @@ let parse_to_dot =
     | Tok.EOI -> ()
     | _ -> dot tok st
   in
-  Pcoq.Entry.of_parser "Coqtoplevel.dot" dot
+  Pcoq.G.Entry.of_parser "Coqtoplevel.dot" dot
 
 (* If an error occurred while parsing, we try to read the input until a dot
    token is encountered.
@@ -255,7 +255,7 @@ let parse_to_dot =
 
 let rec discard_to_dot () =
   try
-    Pcoq.Entry.parse parse_to_dot top_buffer.tokens
+    Pcoq.G.Entry.parse parse_to_dot top_buffer.tokens
   with
     | CLexer.Error.E _ -> discard_to_dot ()
     | e when CErrors.noncritical e -> ()
diff --git a/toplevel/coqloop.mli b/toplevel/coqloop.mli
index 1eafc70530..b07f3e5c57 100644
--- a/toplevel/coqloop.mli
+++ b/toplevel/coqloop.mli
@@ -18,7 +18,7 @@ type input_buffer = {
   mutable str : Bytes.t; (** buffer of already read characters *)
   mutable len : int;    (** number of chars in the buffer *)
   mutable bols : int list; (** offsets in str of beginning of lines *)
-  mutable tokens : Pcoq.Parsable.t; (** stream of tokens *)
+  mutable tokens : Pcoq.G.Parsable.t; (** stream of tokens *)
   mutable start : int } (** stream count of the first char of the buffer *)
 
 (** The input buffer of stdin. *)
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index 955630f40c..ce4b85c75f 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -88,7 +88,7 @@ let load_vernac_core ~echo ~check ~interactive ~state file =
   let input_cleanup () = close_in in_chan; Option.iter close_in in_echo in
 
   let in_pa =
-    Pcoq.Parsable.make ~loc:(Loc.initial (Loc.InFile file))
+    Pcoq.G.Parsable.make ~loc:(Loc.initial (Loc.InFile file))
       (Stream.of_channel in_chan) in
   let open State in
 
@@ -100,7 +100,7 @@ let load_vernac_core ~echo ~check ~interactive ~state file =
     with
     | None ->
       input_cleanup ();
-      state, ids, Pcoq.Parsable.comment_state in_pa
+      state, ids, Pcoq.G.comment_state in_pa
     | Some ast ->
       (* Printing of AST for -compile-verbose *)
       Option.iter (vernac_echo ?loc:ast.CAst.loc) in_echo;