[parsing] Make grammar extension type 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, 17 insertions, 17 deletions

diff --git a/plugins/ltac/tacentries.ml b/plugins/ltac/tacentries.ml
index 4af5699317..53b5386375 100644
--- a/plugins/ltac/tacentries.ml
+++ b/plugins/ltac/tacentries.ml
@@ -44,11 +44,11 @@ let coincide s pat off =
   !break
 
 let atactic n =
-  if n = 5 then Aentry Pltac.binder_tactic
-  else Aentryl (Pltac.tactic_expr, string_of_int n)
+  if n = 5 then Pcoq.G.Symbol.nterm Pltac.binder_tactic
+  else Pcoq.G.Symbol.nterml Pltac.tactic_expr (string_of_int n)
 
 type entry_name = EntryName :
-  'a raw_abstract_argument_type * (Tacexpr.raw_tactic_expr, _, 'a) Extend.symbol -> entry_name
+  'a raw_abstract_argument_type * (Tacexpr.raw_tactic_expr, _, 'a) Pcoq.symbol -> entry_name
 
 (** Quite ad-hoc *)
 let get_tacentry n m =
@@ -57,8 +57,8 @@ let get_tacentry n m =
     && not (Int.equal m 5) (* Because tactic5 is at binder_tactic *)
     && not (Int.equal m 0) (* Because tactic0 is at simple_tactic *)
   in
-  if check_lvl n then EntryName (rawwit Tacarg.wit_tactic, Aself)
-  else if check_lvl (n + 1) then EntryName (rawwit Tacarg.wit_tactic, Anext)
+  if check_lvl n then EntryName (rawwit Tacarg.wit_tactic, Pcoq.G.Symbol.self)
+  else if check_lvl (n + 1) then EntryName (rawwit Tacarg.wit_tactic, Pcoq.G.Symbol.next)
   else EntryName (rawwit Tacarg.wit_tactic, atactic n)
 
 let get_separator = function
@@ -140,23 +140,23 @@ let head_is_ident tg = match tg.tacgram_prods with
 let rec prod_item_of_symbol lev = function
 | Extend.Ulist1 s ->
   let EntryName (Rawwit typ, e) = prod_item_of_symbol lev s in
-  EntryName (Rawwit (ListArg typ), Alist1 e)
+  EntryName (Rawwit (ListArg typ), Pcoq.G.Symbol.list1 e)
 | Extend.Ulist0 s ->
   let EntryName (Rawwit typ, e) = prod_item_of_symbol lev s in
-  EntryName (Rawwit (ListArg typ), Alist0 e)
+  EntryName (Rawwit (ListArg typ), Pcoq.G.Symbol.list0 e)
 | Extend.Ulist1sep (s, sep) ->
   let EntryName (Rawwit typ, e) = prod_item_of_symbol lev s in
-  EntryName (Rawwit (ListArg typ), Alist1sep (e, Atoken (CLexer.terminal sep)))
+  EntryName (Rawwit (ListArg typ), Pcoq.G.Symbol.list1sep e (Pcoq.G.Symbol.token (CLexer.terminal sep)) false)
 | Extend.Ulist0sep (s, sep) ->
   let EntryName (Rawwit typ, e) = prod_item_of_symbol lev s in
-  EntryName (Rawwit (ListArg typ), Alist0sep (e, Atoken (CLexer.terminal sep)))
+  EntryName (Rawwit (ListArg typ), Pcoq.G.Symbol.list0sep e (Pcoq.G.Symbol.token (CLexer.terminal sep)) false)
 | Extend.Uopt s ->
   let EntryName (Rawwit typ, e) = prod_item_of_symbol lev s in
-  EntryName (Rawwit (OptArg typ), Aopt e)
+  EntryName (Rawwit (OptArg typ), Pcoq.G.Symbol.opt e)
 | Extend.Uentry arg ->
   let ArgT.Any tag = arg in
   let wit = ExtraArg tag in
-  EntryName (Rawwit wit, Extend.Aentry (genarg_grammar wit))
+  EntryName (Rawwit wit, Pcoq.G.Symbol.nterm (genarg_grammar wit))
 | Extend.Uentryl (s, n) ->
   let ArgT.Any tag = s in
   assert (coincide (ArgT.repr tag) "tactic" 0);
@@ -399,19 +399,19 @@ let create_ltac_quotation name cast (e, l) =
   in
   let () = ltac_quotations := String.Set.add name !ltac_quotations in
   let entry = match l with
-  | None -> Aentry e
-  | Some l -> Aentryl (e, string_of_int l)
+  | None -> Pcoq.G.Symbol.nterm e
+  | Some l -> Pcoq.G.Symbol.nterml e (string_of_int l)
   in
 (*   let level = Some "1" in *)
   let level = None in
   let assoc = None in
   let rule =
     Next (Next (Next (Next (Next (Stop,
-      Atoken (CLexer.terminal name)),
-      Atoken (CLexer.terminal ":")),
-      Atoken (CLexer.terminal "(")),
+      Pcoq.G.Symbol.token (CLexer.terminal name)),
+      Pcoq.G.Symbol.token (CLexer.terminal ":")),
+      Pcoq.G.Symbol.token (CLexer.terminal "(")),
       entry),
-      Atoken (CLexer.terminal ")"))
+      Pcoq.G.Symbol.token (CLexer.terminal ")"))
   in
   let action _ v _ _ _ loc = cast (Some loc, v) in
   let gram = (level, assoc, [Rule (rule, action)]) in