[parsing] Make grammar rules private.

After the gramlib merge and the type-safe interface added to it, the
grammar extension type is redundant; we thus make it private as a
first step on consolidating it with the one in gramlib's.

1 files changed, 10 insertions, 0 deletions

diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml
index 5601dcb474..8f7d6d1966 100644
--- a/parsing/pcoq.ml
+++ b/parsing/pcoq.ml
@@ -59,6 +59,7 @@ module G : sig
   val comment_state : Parsable.t -> ((int * int) * string) list
   val level_of_nonterm : ('a,norec,'c) Symbol.t -> string option
   val generalize_symbol : ('a, 'tr, 'c) Symbol.t -> ('a, norec, 'c) symbol option
+  val mk_rule : 'a Tok.p list -> string rules
 
 end with type 'a Entry.t = 'a Extend.entry = struct
 
@@ -253,6 +254,15 @@ end with type 'a Entry.t = 'a Extend.entry = struct
     try Some (generalize_symbol s)
     with SelfSymbol -> None
 
+  let rec mk_rule tok =
+    match tok with
+    | [] ->
+      let stop_e = Stop in
+      Rules (stop_e, fun _ -> (* dropped anyway: *) "")
+    | tkn :: rem ->
+      let Rules (r, f) = mk_rule rem in
+      let r = Rule.next_norec r (Symbol.token tkn) in
+      Rules (r, fun _ -> f)
 end
 
 module Parsable = struct