Introduce a Pcoq.Entry module for functions that ought to be exported.

We deprecate the corresponding functions in Pcoq.Gram. The motivation is
that the Gram module is used as an argument to Camlp5 functors, so that
it is not stable by extension. Enforcing that its type is literally the
one Camlp5 expects ensures robustness to extension statically.

Some really internal functions have been bluntly removed. It is unlikely
that they are used by external plugins.

4 files changed, 11 insertions, 11 deletions

diff --git a/toplevel/coqloop.ml b/toplevel/coqloop.ml
index d7ede1c2e..7ae15ac10 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.Gram.coq_parsable; (* stream of tokens *)
+  mutable tokens : Pcoq.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.Gram.parsable (Stream.from (prompt_char doc ic ibuf));
+  ibuf.tokens <- Pcoq.Parsable.make (Stream.from (prompt_char doc ic ibuf));
   ibuf.start <- 0
 
 (* Functions to print underlined locations from an input buffer. *)
@@ -228,7 +228,7 @@ let top_buffer =
     str = Bytes.empty;
     len = 0;
     bols = [];
-    tokens = Pcoq.Gram.parsable (Stream.of_list []);
+    tokens = Pcoq.Parsable.make (Stream.of_list []);
     start = 0 }
 
 let set_prompt prompt =
@@ -253,7 +253,7 @@ let parse_to_dot =
 
 let rec discard_to_dot () =
   try
-    Pcoq.Gram.entry_parse parse_to_dot top_buffer.tokens
+    Pcoq.Entry.parse parse_to_dot top_buffer.tokens
   with
     | Token.Error _ | CLexer.Error.E _ -> discard_to_dot ()
     | Stm.End_of_input -> raise Stm.End_of_input
diff --git a/toplevel/coqloop.mli b/toplevel/coqloop.mli
index 5c07a8bf3..b11f13d3c 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 begining of lines *)
-  mutable tokens : Pcoq.Gram.coq_parsable; (** stream of tokens *)
+  mutable tokens : Pcoq.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/g_toplevel.mlg b/toplevel/g_toplevel.mlg
index 53d3eef23..5aba3d6b0 100644
--- a/toplevel/g_toplevel.mlg
+++ b/toplevel/g_toplevel.mlg
@@ -21,9 +21,9 @@ type vernac_toplevel =
   | VernacControl of vernac_control
 
 module Toplevel_ : sig
-  val vernac_toplevel : vernac_toplevel CAst.t Gram.entry
+  val vernac_toplevel : vernac_toplevel CAst.t Entry.t
 end = struct
-  let gec_vernac s = Gram.entry_create ("toplevel:" ^ s)
+  let gec_vernac s = Entry.create ("toplevel:" ^ s)
   let vernac_toplevel = gec_vernac "vernac_toplevel"
 end
 
@@ -49,6 +49,6 @@ END
 
 {
 
-let parse_toplevel pa = Pcoq.Gram.entry_parse vernac_toplevel pa
+let parse_toplevel pa = Pcoq.Entry.parse vernac_toplevel pa
 
 }
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index c1bbb20d5..c914bbecf 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -121,7 +121,7 @@ let load_vernac_core ~echo ~check ~interactive ~state file =
   let in_echo = if echo then Some (open_utf8_file_in file) else None in
   let input_cleanup () = close_in in_chan; Option.iter close_in in_echo in
 
-  let in_pa   = Pcoq.Gram.parsable ~file:(Loc.InFile file) (Stream.of_channel in_chan) in
+  let in_pa   = Pcoq.Parsable.make ~file:(Loc.InFile file) (Stream.of_channel in_chan) in
   let rstate  = ref state in
   (* For beautify, list of parsed sids *)
   let rids    = ref [] in
@@ -159,12 +159,12 @@ let load_vernac_core ~echo ~check ~interactive ~state file =
       rstate := state;
     done;
     input_cleanup ();
-    !rstate, !rids, Pcoq.Gram.comment_state in_pa
+    !rstate, !rids, Pcoq.Parsable.comment_state in_pa
   with any ->   (* whatever the exception *)
     let (e, info) = CErrors.push any in
     input_cleanup ();
     match e with
-    | Stm.End_of_input -> !rstate, !rids, Pcoq.Gram.comment_state in_pa
+    | Stm.End_of_input -> !rstate, !rids, Pcoq.Parsable.comment_state in_pa
     | reraise -> iraise (e, info)
 
 let process_expr ~state loc_ast =