[pcoq] Inline the exported Gramlib interface instead of exposing it as G

4 files changed, 31 insertions, 31 deletions

diff --git a/plugins/ltac/g_tactic.mlg b/plugins/ltac/g_tactic.mlg
index bec83411c1..5a26ac8827 100644
--- a/plugins/ltac/g_tactic.mlg
+++ b/plugins/ltac/g_tactic.mlg
@@ -62,7 +62,7 @@ open Extraargs
 
 (* idem for (x1..xn:t) [n^2 complexity but exceptional use] *)
 let check_for_coloneq =
-  Pcoq.G.Entry.of_parser "lpar_id_colon"
+  Pcoq.Entry.of_parser "lpar_id_colon"
     (fun _ strm ->
       let rec skip_to_rpar p n =
         match List.last (Stream.npeek n strm) with
diff --git a/plugins/ltac/tacentries.ml b/plugins/ltac/tacentries.ml
index eed7f07b2e..4127d28bae 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 Pcoq.G.Symbol.nterm Pltac.binder_tactic
-  else Pcoq.G.Symbol.nterml Pltac.tactic_expr (string_of_int n)
+  if n = 5 then Pcoq.Symbol.nterm Pltac.binder_tactic
+  else Pcoq.Symbol.nterml Pltac.tactic_expr (string_of_int n)
 
 type entry_name = EntryName :
-  'a raw_abstract_argument_type * (Tacexpr.raw_tactic_expr, _, 'a) Pcoq.G.Symbol.t -> entry_name
+  'a raw_abstract_argument_type * (Tacexpr.raw_tactic_expr, _, 'a) Pcoq.Symbol.t -> 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, Pcoq.G.Symbol.self)
-  else if check_lvl (n + 1) then EntryName (rawwit Tacarg.wit_tactic, Pcoq.G.Symbol.next)
+  if check_lvl n then EntryName (rawwit Tacarg.wit_tactic, Pcoq.Symbol.self)
+  else if check_lvl (n + 1) then EntryName (rawwit Tacarg.wit_tactic, Pcoq.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), Pcoq.G.Symbol.list1 e)
+  EntryName (Rawwit (ListArg typ), Pcoq.Symbol.list1 e)
 | Extend.Ulist0 s ->
   let EntryName (Rawwit typ, e) = prod_item_of_symbol lev s in
-  EntryName (Rawwit (ListArg typ), Pcoq.G.Symbol.list0 e)
+  EntryName (Rawwit (ListArg typ), Pcoq.Symbol.list0 e)
 | Extend.Ulist1sep (s, sep) ->
   let EntryName (Rawwit typ, e) = prod_item_of_symbol lev s in
-  EntryName (Rawwit (ListArg typ), Pcoq.G.Symbol.list1sep e (Pcoq.G.Symbol.token (CLexer.terminal sep)) false)
+  EntryName (Rawwit (ListArg typ), Pcoq.Symbol.list1sep e (Pcoq.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), Pcoq.G.Symbol.list0sep e (Pcoq.G.Symbol.token (CLexer.terminal sep)) false)
+  EntryName (Rawwit (ListArg typ), Pcoq.Symbol.list0sep e (Pcoq.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), Pcoq.G.Symbol.opt e)
+  EntryName (Rawwit (OptArg typ), Pcoq.Symbol.opt e)
 | Extend.Uentry arg ->
   let ArgT.Any tag = arg in
   let wit = ExtraArg tag in
-  EntryName (Rawwit wit, Pcoq.G.Symbol.nterm (genarg_grammar wit))
+  EntryName (Rawwit wit, Pcoq.Symbol.nterm (genarg_grammar wit))
 | Extend.Uentryl (s, n) ->
   let ArgT.Any tag = s in
   assert (coincide (ArgT.repr tag) "tactic" 0);
@@ -191,7 +191,7 @@ let add_tactic_entry (kn, ml, tg) state =
   in
   let prods = List.map map tg.tacgram_prods in
   let rules = make_rule mkact prods in
-  let r = ExtendRule (entry, { G.pos; data=[(None, None, [rules])]}) in
+  let r = ExtendRule (entry, { pos; data=[(None, None, [rules])]}) in
   ([r], state)
 
 let tactic_grammar =
@@ -399,14 +399,14 @@ 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 -> Pcoq.G.Symbol.nterm e
-  | Some l -> Pcoq.G.Symbol.nterml e (string_of_int l)
+  | None -> Pcoq.Symbol.nterm e
+  | Some l -> Pcoq.Symbol.nterml e (string_of_int l)
   in
 (*   let level = Some "1" in *)
   let level = None in
   let assoc = None in
   let rule =
-    Pcoq.G.(
+    Pcoq.(
       Rule.next
         (Rule.next
            (Rule.next
@@ -420,8 +420,8 @@ let create_ltac_quotation name cast (e, l) =
         (Symbol.token (CLexer.terminal ")")))
   in
   let action _ v _ _ _ loc = cast (Some loc, v) in
-  let gram = (level, assoc, [Pcoq.G.Production.make rule action]) in
-  Pcoq.grammar_extend Pltac.tactic_arg {G.pos=None; data=[gram]}
+  let gram = (level, assoc, [Pcoq.Production.make rule action]) in
+  Pcoq.grammar_extend Pltac.tactic_arg {pos=None; data=[gram]}
 
 (** Command *)
 
@@ -765,7 +765,7 @@ let argument_extend (type a b c) ~name (arg : (a, b, c) tactic_argument) =
     e
   | Vernacextend.Arg_rules rules ->
     let e = Pcoq.create_generic_entry Pcoq.utactic name (Genarg.rawwit wit) in
-    let () = Pcoq.grammar_extend e {G.pos=None; data=[(None, None, rules)]} in
+    let () = Pcoq.grammar_extend e {pos=None; data=[(None, None, rules)]} in
     e
   in
   let (rpr, gpr, tpr) = arg.arg_printer in
diff --git a/plugins/ssr/ssrparser.mlg b/plugins/ssr/ssrparser.mlg
index c3396584a4..442b40221b 100644
--- a/plugins/ssr/ssrparser.mlg
+++ b/plugins/ssr/ssrparser.mlg
@@ -263,16 +263,16 @@ let negate_parser f tok x =
   | Some _ -> raise Stream.Failure
 
 let test_not_ssrslashnum =
-  Pcoq.G.Entry.of_parser
+  Pcoq.Entry.of_parser
     "test_not_ssrslashnum" (negate_parser test_ssrslashnum10)
 let test_ssrslashnum00 =
-  Pcoq.G.Entry.of_parser "test_ssrslashnum01" test_ssrslashnum00
+  Pcoq.Entry.of_parser "test_ssrslashnum01" test_ssrslashnum00
 let test_ssrslashnum10 =
-  Pcoq.G.Entry.of_parser "test_ssrslashnum10" test_ssrslashnum10
+  Pcoq.Entry.of_parser "test_ssrslashnum10" test_ssrslashnum10
 let test_ssrslashnum11 =
-  Pcoq.G.Entry.of_parser "test_ssrslashnum11" test_ssrslashnum11
+  Pcoq.Entry.of_parser "test_ssrslashnum11" test_ssrslashnum11
 let test_ssrslashnum01 =
-  Pcoq.G.Entry.of_parser "test_ssrslashnum01" test_ssrslashnum01
+  Pcoq.Entry.of_parser "test_ssrslashnum01" test_ssrslashnum01
 
 }
 
@@ -459,7 +459,7 @@ let input_ssrtermkind _ strm = match Util.stream_nth 0 strm with
   | Tok.KEYWORD "@" -> xWithAt
   | _ -> xNoFlag
 
-let ssrtermkind = Pcoq.G.Entry.of_parser "ssrtermkind" input_ssrtermkind
+let ssrtermkind = Pcoq.Entry.of_parser "ssrtermkind" input_ssrtermkind
 
 (* New kinds of terms *)
 
@@ -470,7 +470,7 @@ let input_term_annotation _ strm =
   | Tok.KEYWORD "@" :: _ -> `At
   | _ -> `None
 let term_annotation =
-  Pcoq.G.Entry.of_parser "term_annotation" input_term_annotation
+  Pcoq.Entry.of_parser "term_annotation" input_term_annotation
 
 (* terms *)
 
@@ -811,7 +811,7 @@ let reject_ssrhid _ strm =
       | _ -> ())
   | _ -> ()
 
-let test_nohidden = Pcoq.G.Entry.of_parser "test_ssrhid" reject_ssrhid
+let test_nohidden = Pcoq.Entry.of_parser "test_ssrhid" reject_ssrhid
 
 let rec reject_binder crossed_paren k tok s =
   match
@@ -825,7 +825,7 @@ let rec reject_binder crossed_paren k tok s =
   | Some (Tok.KEYWORD ")") when crossed_paren -> raise Stream.Failure
   | _ -> if crossed_paren then () else raise Stream.Failure
 
-let _test_nobinder = Pcoq.G.Entry.of_parser "test_nobinder" (reject_binder false 0)
+let _test_nobinder = Pcoq.Entry.of_parser "test_nobinder" (reject_binder false 0)
 
 }
 
@@ -1659,7 +1659,7 @@ let ssr_id_of_string loc s =
   ^ "Scripts with explicit references to anonymous variables are fragile."))
     end; Id.of_string s
 
-let ssr_null_entry = Pcoq.G.Entry.of_parser "ssr_null" (fun _ _ -> ())
+let ssr_null_entry = Pcoq.Entry.of_parser "ssr_null" (fun _ _ -> ())
 
 }
 
@@ -2382,7 +2382,7 @@ let test_ssr_rw_syntax =
     match Util.stream_nth 0 strm with
     | Tok.KEYWORD key when List.mem key.[0] [lbrace; '['; '/'] -> ()
     | _ -> raise Stream.Failure in
-  Pcoq.G.Entry.of_parser "test_ssr_rw_syntax" test
+  Pcoq.Entry.of_parser "test_ssr_rw_syntax" test
 
 }
 
diff --git a/plugins/ssrmatching/g_ssrmatching.mlg b/plugins/ssrmatching/g_ssrmatching.mlg
index 59abf80dc5..33e523a4a4 100644
--- a/plugins/ssrmatching/g_ssrmatching.mlg
+++ b/plugins/ssrmatching/g_ssrmatching.mlg
@@ -70,7 +70,7 @@ let input_ssrtermkind _ strm = match Util.stream_nth 0 strm with
   | Tok.KEYWORD "(" -> '('
   | Tok.KEYWORD "@" -> '@'
   | _ -> ' '
-let ssrtermkind = Pcoq.G.Entry.of_parser "ssrtermkind" input_ssrtermkind
+let ssrtermkind = Pcoq.Entry.of_parser "ssrtermkind" input_ssrtermkind
 
 }