2 files changed, 14 insertions, 10 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
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index 63a4c1dd58..e7e3e9442b 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -224,20 +224,13 @@ module Module :
 (** {5 Type-safe grammar extension} *)
 
 type ('self, 'trec, 'a) symbol
+type ('self, 'trec, _, 'r) rule
 
 type norec = Gramlib.Grammar.norec
 type mayrec = Gramlib.Grammar.mayrec
 
-type ('self, 'trec, _, 'r) rule =
-| Stop : ('self, norec, 'r, 'r) rule
-| Next : ('self, _, 'a, 'r) rule * ('self, _, 'b) symbol -> ('self, mayrec, 'b -> 'a, 'r) rule
-| NextNoRec : ('self, norec, 'a, 'r) rule * ('self, norec, 'b) symbol -> ('self, norec, 'b -> 'a, 'r) rule
-
-type 'a rules =
-  | Rules : (_, norec, 'act, Loc.t -> 'a) rule * 'act -> 'a rules
-
-type 'a production_rule =
-  | Rule : ('a, _, 'act, Loc.t -> 'a) rule * 'act -> 'a production_rule
+type 'a rules
+type 'a production_rule
 
 module G : sig
 
@@ -245,6 +238,7 @@ module G : sig
 
   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 Entry.t
      and type te = Tok.t