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

3 files changed, 16 insertions, 23 deletions

diff --git a/vernac/egramcoq.ml b/vernac/egramcoq.ml
index ba542101c8..43029f4d53 100644
--- a/vernac/egramcoq.ml
+++ b/vernac/egramcoq.ml
@@ -328,15 +328,7 @@ let make_sep_rules = function
   | [tk] ->
     Pcoq.G.Symbol.token tk
   | tkl ->
-    let rec mkrule : 'a Tok.p list -> 'a rules = function
-      | [] ->
-        Rules (Stop, fun _ -> (* dropped anyway: *) "")
-      | tkn :: rem ->
-        let Rules (r, f) = mkrule rem in
-        let r = NextNoRec (r, Pcoq.G.Symbol.token tkn) in
-        Rules (r, fun _ -> f)
-    in
-    let r = mkrule (List.rev tkl) in
+    let r = Pcoq.G.mk_rule (List.rev tkl) in
     Pcoq.G.Symbol.rules ~warning:None [r]
 
 type ('s, 'a) mayrec_symbol =
@@ -470,18 +462,18 @@ type ('s, 'a, 'r) mayrec_rule =
 | MayRecRMay : ('s, mayrec, 'a, 'r) rule -> ('s, 'a, 'r) mayrec_rule
 
 let rec ty_erase : type s a r. (s, a, r) ty_rule -> (s, a, r) mayrec_rule = function
-| TyStop -> MayRecRNo Stop
+| TyStop -> MayRecRNo G.Rule.stop
 | TyMark (_, _, _, r) -> ty_erase r
 | TyNext (rem, TyTerm tok) ->
    begin match ty_erase rem with
-   | MayRecRNo rem -> MayRecRMay (Next (rem, Pcoq.G.Symbol.token tok))
-   | MayRecRMay rem -> MayRecRMay (Next (rem, Pcoq.G.Symbol.token tok)) end
+   | MayRecRNo rem -> MayRecRMay (G.Rule.next rem (G.Symbol.token tok))
+   | MayRecRMay rem -> MayRecRMay (G.Rule.next rem (G.Symbol.token tok)) end
 | TyNext (rem, TyNonTerm (_, _, s, _)) ->
    begin match ty_erase rem, s with
-   | MayRecRNo rem, MayRecNo s -> MayRecRMay (Next (rem, s))
-   | MayRecRNo rem, MayRecMay s -> MayRecRMay (Next (rem, s))
-   | MayRecRMay rem, MayRecNo s -> MayRecRMay (Next (rem, s))
-   | MayRecRMay rem, MayRecMay s -> MayRecRMay (Next (rem, s)) end
+   | MayRecRNo rem, MayRecNo s -> MayRecRMay (G.Rule.next rem s)
+   | MayRecRNo rem, MayRecMay s -> MayRecRMay (G.Rule.next rem s)
+   | MayRecRMay rem, MayRecNo s -> MayRecRMay (G.Rule.next rem s)
+   | MayRecRMay rem, MayRecMay s -> MayRecRMay (G.Rule.next rem s) end
 
 type ('self, 'r) any_ty_rule =
 | AnyTyRule : ('self, 'act, Loc.t -> 'r) ty_rule -> ('self, 'r) any_ty_rule
@@ -564,8 +556,9 @@ let extend_constr state forpat ng =
     let act = ty_eval r (make_act forpat ng.notgram_notation) empty in
     let rule =
       let r = match ty_erase r with
-        | MayRecRNo symbs -> Rule (symbs, act)
-        | MayRecRMay symbs -> Rule (symbs, act) in
+        | MayRecRNo symbs -> Pcoq.G.Production.make symbs act
+        | MayRecRMay symbs -> Pcoq.G.Production.make symbs act
+      in
       name, p4assoc, [r] in
     let r = match reinit with
       | None ->
diff --git a/vernac/egramml.ml b/vernac/egramml.ml
index bcd8de1ff4..175217803f 100644
--- a/vernac/egramml.ml
+++ b/vernac/egramml.ml
@@ -45,8 +45,8 @@ let rec ty_rule_of_gram = function
   AnyTyRule r
 
 let rec ty_erase : type s tr a r. (s, tr, a, r) ty_rule -> (s, tr, a, r) Pcoq.rule = function
-| TyStop -> Pcoq.Stop
-| TyNext (rem, tok, _) -> Pcoq.Next (ty_erase rem, tok)
+| TyStop -> Pcoq.G.Rule.stop
+| TyNext (rem, tok, _) -> Pcoq.G.Rule.next (ty_erase rem) tok
 
 type 'r gen_eval = Loc.t -> raw_generic_argument list -> 'r
 
@@ -62,7 +62,7 @@ let make_rule f prod =
   let symb = ty_erase ty_rule in
   let f loc l = f loc (List.rev l) in
   let act = ty_eval ty_rule f in
-  Pcoq.Rule (symb, act)
+  Pcoq.G.Production.make symb act
 
 let rec proj_symbol : type a b c. (a, b, c) ty_user_symbol -> (a, b, c) genarg_type = function
 | TUentry a -> ExtraArg a
diff --git a/vernac/pvernac.ml b/vernac/pvernac.ml
index aebded72f8..27b8a5bda2 100644
--- a/vernac/pvernac.ml
+++ b/vernac/pvernac.ml
@@ -54,8 +54,8 @@ module Vernac_ =
       let act_vernac v loc = Some v in
       let act_eoi _ loc = None in
       let rule = [
-        Rule (Next (Stop, Pcoq.G.Symbol.token Tok.PEOI), act_eoi);
-        Rule (Next (Stop, Pcoq.G.Symbol.nterm vernac_control), act_vernac);
+        Pcoq.G.(Production.make (Rule.next Rule.stop (Symbol.token Tok.PEOI)) act_eoi);
+        Pcoq.G.(Production.make (Rule.next Rule.stop (Symbol.nterm vernac_control)) act_vernac);
       ] in
       Pcoq.grammar_extend main_entry (None, [None, None, rule])