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.

9 files changed, 35 insertions, 35 deletions

diff --git a/vernac/egramcoq.ml b/vernac/egramcoq.ml
index 48f225f97..3281b75aa 100644
--- a/vernac/egramcoq.ml
+++ b/vernac/egramcoq.ml
@@ -240,14 +240,14 @@ type (_, _) entry =
 type _ any_entry = TTAny : ('s, 'r) entry -> 's any_entry
 
 (* This computes the name of the level where to add a new rule *)
-let interp_constr_entry_key : type r. r target -> int -> r Gram.entry * int option =
+let interp_constr_entry_key : type r. r target -> int -> r Entry.t * int option =
   fun forpat level -> match forpat with
   | ForConstr ->
     if level = 200 then Constr.binder_constr, None
     else Constr.operconstr, Some level
   | ForPattern -> Constr.pattern, Some level
 
-let target_entry : type s. s target -> s Gram.entry = function
+let target_entry : type s. s target -> s Entry.t = function
 | ForConstr -> Constr.operconstr
 | ForPattern -> Constr.pattern
 
diff --git a/vernac/egramml.mli b/vernac/egramml.mli
index 31aa1a989..a5ee036db 100644
--- a/vernac/egramml.mli
+++ b/vernac/egramml.mli
@@ -21,7 +21,7 @@ type 's grammar_prod_item =
       ('s, 'a) Extend.symbol) Loc.located -> 's grammar_prod_item
 
 val extend_vernac_command_grammar :
-  Vernacexpr.extend_name -> vernac_expr Pcoq.Gram.entry option ->
+  Vernacexpr.extend_name -> vernac_expr Pcoq.Entry.t option ->
     vernac_expr grammar_prod_item list -> unit
 
 val get_extend_vernac_rule : Vernacexpr.extend_name -> vernac_expr grammar_prod_item list
diff --git a/vernac/g_proofs.mlg b/vernac/g_proofs.mlg
index cccdbfc91..dacef6e21 100644
--- a/vernac/g_proofs.mlg
+++ b/vernac/g_proofs.mlg
@@ -22,7 +22,7 @@ open Pvernac.Vernac_
 
 let thm_token = G_vernac.thm_token
 
-let hint = Gram.entry_create "hint"
+let hint = Entry.create "hint"
 
 let warn_deprecated_focus =
   CWarnings.create ~name:"deprecated-focus" ~category:"deprecated"
diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg
index 3a01ce6df..2c60abfe3 100644
--- a/vernac/g_vernac.mlg
+++ b/vernac/g_vernac.mlg
@@ -37,18 +37,18 @@ let _ = List.iter CLexer.add_keyword vernac_kw
 (* Rem: do not join the different GEXTEND into one, it breaks native *)
 (* compilation on PowerPC and Sun architectures *)
 
-let query_command = Gram.entry_create "vernac:query_command"
-
-let subprf = Gram.entry_create "vernac:subprf"
-
-let class_rawexpr = Gram.entry_create "vernac:class_rawexpr"
-let thm_token = Gram.entry_create "vernac:thm_token"
-let def_body = Gram.entry_create "vernac:def_body"
-let decl_notation = Gram.entry_create "vernac:decl_notation"
-let record_field = Gram.entry_create "vernac:record_field"
-let of_type_with_opt_coercion = Gram.entry_create "vernac:of_type_with_opt_coercion"
-let instance_name = Gram.entry_create "vernac:instance_name"
-let section_subset_expr = Gram.entry_create "vernac:section_subset_expr"
+let query_command = Entry.create "vernac:query_command"
+
+let subprf = Entry.create "vernac:subprf"
+
+let class_rawexpr = Entry.create "vernac:class_rawexpr"
+let thm_token = Entry.create "vernac:thm_token"
+let def_body = Entry.create "vernac:def_body"
+let decl_notation = Entry.create "vernac:decl_notation"
+let record_field = Entry.create "vernac:record_field"
+let of_type_with_opt_coercion = Entry.create "vernac:of_type_with_opt_coercion"
+let instance_name = Entry.create "vernac:instance_name"
+let section_subset_expr = Entry.create "vernac:section_subset_expr"
 
 let make_bullet s =
   let open Proof_bullet in
diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml
index 240147c8d..33e6229b2 100644
--- a/vernac/metasyntax.ml
+++ b/vernac/metasyntax.ml
@@ -49,7 +49,7 @@ let entry_buf = Buffer.create 64
 let pr_entry e =
   let () = Buffer.clear entry_buf in
   let ft = Format.formatter_of_buffer entry_buf in
-  let () = Pcoq.Gram.entry_print ft e in
+  let () = Pcoq.Entry.print ft e in
   str (Buffer.contents entry_buf)
 
 let pr_registered_grammar name =
diff --git a/vernac/proof_using.ml b/vernac/proof_using.ml
index f8b085f3e..74e53bef1 100644
--- a/vernac/proof_using.ml
+++ b/vernac/proof_using.ml
@@ -178,7 +178,7 @@ let suggest_variable env id =
 let value = ref None
 
 let using_to_string us = Pp.string_of_ppcmds (Ppvernac.pr_using us)
-let using_from_string us = Pcoq.Gram.(entry_parse G_vernac.section_subset_expr (parsable (Stream.of_string us)))
+let using_from_string us = Pcoq.Entry.parse G_vernac.section_subset_expr (Pcoq.Parsable.make (Stream.of_string us))
 
 let _ =
   Goptions.declare_stringopt_option
diff --git a/vernac/pvernac.ml b/vernac/pvernac.ml
index aea66a07a..b2fa8ec99 100644
--- a/vernac/pvernac.ml
+++ b/vernac/pvernac.ml
@@ -14,7 +14,7 @@ let uvernac = create_universe "vernac"
 
 module Vernac_ =
   struct
-    let gec_vernac s = Gram.entry_create ("vernac:" ^ s)
+    let gec_vernac s = Entry.create ("vernac:" ^ s)
 
     (* The different kinds of vernacular commands *)
     let gallina = gec_vernac "gallina"
@@ -26,7 +26,7 @@ module Vernac_ =
     let red_expr = new_entry utactic "red_expr"
     let hint_info = gec_vernac "hint_info"
     (* Main vernac entry *)
-    let main_entry = Gram.entry_create "vernac"
+    let main_entry = Entry.create "vernac"
     let noedit_mode = gec_vernac "noedit_command"
 
     let () =
diff --git a/vernac/pvernac.mli b/vernac/pvernac.mli
index 2993a1661..b2f8f7146 100644
--- a/vernac/pvernac.mli
+++ b/vernac/pvernac.mli
@@ -16,21 +16,21 @@ val uvernac : gram_universe
 
 module Vernac_ :
   sig
-    val gallina : vernac_expr Gram.entry
-    val gallina_ext : vernac_expr Gram.entry
-    val command : vernac_expr Gram.entry
-    val syntax : vernac_expr Gram.entry
-    val vernac_control : vernac_control Gram.entry
-    val rec_definition : (fixpoint_expr * decl_notation list) Gram.entry
-    val noedit_mode : vernac_expr Gram.entry
-    val command_entry : vernac_expr Gram.entry
-    val red_expr : raw_red_expr Gram.entry
-    val hint_info : Hints.hint_info_expr Gram.entry
+    val gallina : vernac_expr Entry.t
+    val gallina_ext : vernac_expr Entry.t
+    val command : vernac_expr Entry.t
+    val syntax : vernac_expr Entry.t
+    val vernac_control : vernac_control Entry.t
+    val rec_definition : (fixpoint_expr * decl_notation list) Entry.t
+    val noedit_mode : vernac_expr Entry.t
+    val command_entry : vernac_expr Entry.t
+    val red_expr : raw_red_expr Entry.t
+    val hint_info : Hints.hint_info_expr Entry.t
   end
 
 (** The main entry: reads an optional vernac command *)
-val main_entry : (Loc.t * vernac_control) option Gram.entry
+val main_entry : (Loc.t * vernac_control) option Entry.t
 
 (** Handling of the proof mode entry *)
-val get_command_entry : unit -> vernac_expr Gram.entry
-val set_command_entry : vernac_expr Gram.entry -> unit
+val get_command_entry : unit -> vernac_expr Entry.t
+val set_command_entry : vernac_expr Entry.t -> unit
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 5fda1a0da..8064856a6 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -2040,7 +2040,7 @@ let vernac_load interp fname =
     interp x in
   let parse_sentence = Flags.with_option Flags.we_are_parsing
     (fun po ->
-    match Pcoq.Gram.entry_parse Pvernac.main_entry po with
+    match Pcoq.Entry.parse Pvernac.main_entry po with
       | Some x -> x
       | None -> raise End_of_input) in
   let fname =
@@ -2049,7 +2049,7 @@ let vernac_load interp fname =
   let input =
     let longfname = Loadpath.locate_file fname in
     let in_chan = open_utf8_file_in longfname in
-    Pcoq.Gram.parsable ~file:(Loc.InFile longfname) (Stream.of_channel in_chan) in
+    Pcoq.Parsable.make ~file:(Loc.InFile longfname) (Stream.of_channel in_chan) in
   begin
     try while true do interp (snd (parse_sentence input)) done
     with End_of_input -> ()