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

11 files changed, 70 insertions, 70 deletions

diff --git a/vernac/egramcoq.ml b/vernac/egramcoq.ml
index c4f15a40ce..fdc8b1ba4c 100644
--- a/vernac/egramcoq.ml
+++ b/vernac/egramcoq.ml
@@ -326,47 +326,47 @@ let is_binder_level custom (custom',from) e = match e with
 
 let make_sep_rules = function
   | [tk] ->
-    Pcoq.G.Symbol.token tk
+    Pcoq.Symbol.token tk
   | tkl ->
-    let r = Pcoq.G.mk_rule (List.rev tkl) in
-    Pcoq.G.Symbol.rules [r]
+    let r = Pcoq.mk_rule (List.rev tkl) in
+    Pcoq.Symbol.rules [r]
 
 type ('s, 'a) mayrec_symbol =
-| MayRecNo : ('s, Gramlib.Grammar.norec, 'a) G.Symbol.t -> ('s, 'a) mayrec_symbol
-| MayRecMay : ('s, Gramlib.Grammar.mayrec, 'a) G.Symbol.t -> ('s, 'a) mayrec_symbol
+| MayRecNo : ('s, Gramlib.Grammar.norec, 'a) Symbol.t -> ('s, 'a) mayrec_symbol
+| MayRecMay : ('s, Gramlib.Grammar.mayrec, 'a) Symbol.t -> ('s, 'a) mayrec_symbol
 
 let symbol_of_target : type s. _ -> _ -> _ -> _ -> s target -> (s, s) mayrec_symbol = fun custom p assoc from forpat ->
   if is_binder_level custom from p
   then
     (* Prevent self *)
-    MayRecNo (Pcoq.G.Symbol.nterml (target_entry custom forpat) "200")
-  else if is_self custom from p then MayRecMay Pcoq.G.Symbol.self
+    MayRecNo (Pcoq.Symbol.nterml (target_entry custom forpat) "200")
+  else if is_self custom from p then MayRecMay Pcoq.Symbol.self
   else
     let g = target_entry custom forpat in
     let lev = adjust_level custom assoc from p in
     begin match lev with
-    | DefaultLevel -> MayRecNo (Pcoq.G.Symbol.nterm g)
-    | NextLevel -> MayRecMay Pcoq.G.Symbol.next
-    | NumLevel lev -> MayRecNo (Pcoq.G.Symbol.nterml g (string_of_int lev))
+    | DefaultLevel -> MayRecNo (Pcoq.Symbol.nterm g)
+    | NextLevel -> MayRecMay Pcoq.Symbol.next
+    | NumLevel lev -> MayRecNo (Pcoq.Symbol.nterml g (string_of_int lev))
     end
 
 let symbol_of_entry : type s r. _ -> _ -> (s, r) entry -> (s, r) mayrec_symbol = fun assoc from typ -> match typ with
 | TTConstr (s, p, forpat) -> symbol_of_target s p assoc from forpat
 | TTConstrList (s, typ', [], forpat) ->
   begin match symbol_of_target s typ' assoc from forpat with
-  | MayRecNo s -> MayRecNo (Pcoq.G.Symbol.list1 s)
-  | MayRecMay s -> MayRecMay (Pcoq.G.Symbol.list1 s) end
+  | MayRecNo s -> MayRecNo (Pcoq.Symbol.list1 s)
+  | MayRecMay s -> MayRecMay (Pcoq.Symbol.list1 s) end
 | TTConstrList (s, typ', tkl, forpat) ->
   begin match symbol_of_target s typ' assoc from forpat with
-  | MayRecNo s -> MayRecNo (Pcoq.G.Symbol.list1sep s (make_sep_rules tkl) false)
-  | MayRecMay s -> MayRecMay (Pcoq.G.Symbol.list1sep s (make_sep_rules tkl) false) end
-| TTPattern p -> MayRecNo (Pcoq.G.Symbol.nterml Constr.pattern (string_of_int p))
-| TTClosedBinderList [] -> MayRecNo (Pcoq.G.Symbol.list1 (Pcoq.G.Symbol.nterm Constr.binder))
-| TTClosedBinderList tkl -> MayRecNo (Pcoq.G.Symbol.list1sep (Pcoq.G.Symbol.nterm Constr.binder) (make_sep_rules tkl) false)
-| TTName -> MayRecNo (Pcoq.G.Symbol.nterm Prim.name)
-| TTOpenBinderList -> MayRecNo (Pcoq.G.Symbol.nterm Constr.open_binders)
-| TTBigint -> MayRecNo (Pcoq.G.Symbol.nterm Prim.bignat)
-| TTReference -> MayRecNo (Pcoq.G.Symbol.nterm Constr.global)
+  | MayRecNo s -> MayRecNo (Pcoq.Symbol.list1sep s (make_sep_rules tkl) false)
+  | MayRecMay s -> MayRecMay (Pcoq.Symbol.list1sep s (make_sep_rules tkl) false) end
+| TTPattern p -> MayRecNo (Pcoq.Symbol.nterml Constr.pattern (string_of_int p))
+| TTClosedBinderList [] -> MayRecNo (Pcoq.Symbol.list1 (Pcoq.Symbol.nterm Constr.binder))
+| TTClosedBinderList tkl -> MayRecNo (Pcoq.Symbol.list1sep (Pcoq.Symbol.nterm Constr.binder) (make_sep_rules tkl) false)
+| TTName -> MayRecNo (Pcoq.Symbol.nterm Prim.name)
+| TTOpenBinderList -> MayRecNo (Pcoq.Symbol.nterm Constr.open_binders)
+| TTBigint -> MayRecNo (Pcoq.Symbol.nterm Prim.bignat)
+| TTReference -> MayRecNo (Pcoq.Symbol.nterm Constr.global)
 
 let interp_entry forpat e = match e with
 | ETProdName -> TTAny TTName
@@ -458,22 +458,22 @@ let rec ty_eval : type s a. (s, a, Loc.t -> s) ty_rule -> s gen_eval -> s env ->
     ty_eval rem f { env with constrs; constrlists; }
 
 type ('s, 'a, 'r) mayrec_rule =
-| MayRecRNo : ('s, Gramlib.Grammar.norec, 'a, 'r) G.Rule.t -> ('s, 'a, 'r) mayrec_rule
-| MayRecRMay : ('s, Gramlib.Grammar.mayrec, 'a, 'r) G.Rule.t -> ('s, 'a, 'r) mayrec_rule
+| MayRecRNo : ('s, Gramlib.Grammar.norec, 'a, 'r) Rule.t -> ('s, 'a, 'r) mayrec_rule
+| MayRecRMay : ('s, Gramlib.Grammar.mayrec, 'a, 'r) Rule.t -> ('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 G.Rule.stop
+| TyStop -> MayRecRNo Rule.stop
 | TyMark (_, _, _, r) -> ty_erase r
 | TyNext (rem, TyTerm tok) ->
    begin match ty_erase rem with
-   | MayRecRNo rem -> MayRecRMay (G.Rule.next rem (G.Symbol.token tok))
-   | MayRecRMay rem -> MayRecRMay (G.Rule.next rem (G.Symbol.token tok)) end
+   | MayRecRNo rem -> MayRecRMay (Rule.next rem (Symbol.token tok))
+   | MayRecRMay rem -> MayRecRMay (Rule.next rem (Symbol.token tok)) end
 | TyNext (rem, TyNonTerm (_, _, s, _)) ->
    begin match ty_erase rem, s with
-   | 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
+   | MayRecRNo rem, MayRecNo s -> MayRecRMay (Rule.next rem s)
+   | MayRecRNo rem, MayRecMay s -> MayRecRMay (Rule.next rem s)
+   | MayRecRMay rem, MayRecNo s -> MayRecRMay (Rule.next rem s)
+   | MayRecRMay rem, MayRecMay s -> MayRecRMay (Rule.next rem s) end
 
 type ('self, 'r) any_ty_rule =
 | AnyTyRule : ('self, 'act, Loc.t -> 'r) ty_rule -> ('self, 'r) any_ty_rule
@@ -501,7 +501,7 @@ let target_to_bool : type r. r target -> bool = function
 | ForPattern -> true
 
 let prepare_empty_levels forpat (where,(pos,p4assoc,name,reinit)) =
-  let empty = { G.pos; data = [(name, p4assoc, [])] } in
+  let empty = { pos; data = [(name, p4assoc, [])] } in
   match reinit with
   | None ->
     ExtendRule (target_entry where forpat, empty)
@@ -520,7 +520,7 @@ let rec pure_sublevels' assoc from forpat level = function
    let push where p rem =
      match symbol_of_target where p assoc from forpat with
      | MayRecNo sym ->
-       (match Pcoq.G.level_of_nonterm sym with
+       (match Pcoq.level_of_nonterm sym with
         | None -> rem
         | Some i ->
           if different_levels (fst from,level) (where,i) then
@@ -556,15 +556,15 @@ 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 -> Pcoq.G.Production.make symbs act
-        | MayRecRMay symbs -> Pcoq.G.Production.make symbs act
+        | MayRecRNo symbs -> Pcoq.Production.make symbs act
+        | MayRecRMay symbs -> Pcoq.Production.make symbs act
       in
       name, p4assoc, [r] in
     let r = match reinit with
       | None ->
-        ExtendRule (entry, { G.pos; data = [rule]})
+        ExtendRule (entry, { pos; data = [rule]})
       | Some reinit ->
-        ExtendRuleReinit (entry, reinit, { G.pos; data = [rule]})
+        ExtendRuleReinit (entry, reinit, { pos; data = [rule]})
     in
     (accu @ empty_rules @ [r], state)
   in
diff --git a/vernac/egramml.ml b/vernac/egramml.ml
index 981de78162..bda1401bc9 100644
--- a/vernac/egramml.ml
+++ b/vernac/egramml.ml
@@ -19,13 +19,13 @@ open Vernacexpr
 type 's grammar_prod_item =
   | GramTerminal of string
   | GramNonTerminal :
-      ('a raw_abstract_argument_type * ('s, _, 'a) G.Symbol.t) Loc.located -> 's grammar_prod_item
+      ('a raw_abstract_argument_type * ('s, _, 'a) Symbol.t) Loc.located -> 's grammar_prod_item
 
 type 'a ty_arg = ('a -> raw_generic_argument)
 
 type ('self, 'tr, _, 'r) ty_rule =
 | TyStop : ('self, Gramlib.Grammar.norec, 'r, 'r) ty_rule
-| TyNext : ('self, _, 'a, 'r) ty_rule * ('self, _, 'b) G.Symbol.t * 'b ty_arg option ->
+| TyNext : ('self, _, 'a, 'r) ty_rule * ('self, _, 'b) Symbol.t * 'b ty_arg option ->
   ('self, Gramlib.Grammar.mayrec, 'b -> 'a, 'r) ty_rule
 
 type ('self, 'r) any_ty_rule =
@@ -35,7 +35,7 @@ let rec ty_rule_of_gram = function
 | [] -> AnyTyRule TyStop
 | GramTerminal s :: rem ->
   let AnyTyRule rem = ty_rule_of_gram rem in
-  let tok = Pcoq.G.Symbol.token (CLexer.terminal s) in
+  let tok = Pcoq.Symbol.token (CLexer.terminal s) in
   let r = TyNext (rem, tok, None) in
   AnyTyRule r
 | GramNonTerminal (_, (t, tok)) :: rem ->
@@ -44,9 +44,9 @@ let rec ty_rule_of_gram = function
   let r = TyNext (rem, tok, inj) in
   AnyTyRule r
 
-let rec ty_erase : type s tr a r. (s, tr, a, r) ty_rule -> (s, tr, a, r) Pcoq.G.Rule.t = function
-| TyStop -> Pcoq.G.Rule.stop
-| TyNext (rem, tok, _) -> Pcoq.G.Rule.next (ty_erase rem) tok
+let rec ty_erase : type s tr a r. (s, tr, a, r) ty_rule -> (s, tr, a, r) Pcoq.Rule.t = function
+| TyStop -> Pcoq.Rule.stop
+| TyNext (rem, tok, _) -> Pcoq.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.G.Production.make symb act
+  Pcoq.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
@@ -90,4 +90,4 @@ let extend_vernac_command_grammar s nt gl =
   vernac_exts := (s,gl) :: !vernac_exts;
   let mkact loc l = VernacExtend (s, l) in
   let rules = [make_rule mkact gl] in
-  grammar_extend nt { G.pos=None; data=[None, None, rules]}
+  grammar_extend nt { pos=None; data=[None, None, rules]}
diff --git a/vernac/egramml.mli b/vernac/egramml.mli
index 77198452b9..15f415ca3b 100644
--- a/vernac/egramml.mli
+++ b/vernac/egramml.mli
@@ -18,7 +18,7 @@ open Vernacexpr
 type 's grammar_prod_item =
   | GramTerminal of string
   | GramNonTerminal : ('a Genarg.raw_abstract_argument_type *
-      ('s, _, 'a) Pcoq.G.Symbol.t) Loc.located -> 's grammar_prod_item
+      ('s, _, 'a) Pcoq.Symbol.t) Loc.located -> 's grammar_prod_item
 
 val extend_vernac_command_grammar :
   extend_name -> vernac_expr Pcoq.Entry.t option ->
@@ -32,4 +32,4 @@ val proj_symbol : ('a, 'b, 'c) Extend.ty_user_symbol -> ('a, 'b, 'c) Genarg.gena
 
 val make_rule :
   (Loc.t -> Genarg.raw_generic_argument list -> 'a) ->
-  'a grammar_prod_item list -> 'a Pcoq.G.Production.t
+  'a grammar_prod_item list -> 'a Pcoq.Production.t
diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml
index 38e57a310a..475d5c31f7 100644
--- a/vernac/metasyntax.ml
+++ b/vernac/metasyntax.ml
@@ -46,7 +46,7 @@ let entry_buf = Buffer.create 64
 let pr_entry e =
   let () = Buffer.clear entry_buf in
   let ft = Format.formatter_of_buffer entry_buf in
-  let () = Pcoq.G.Entry.print ft e in
+  let () = Pcoq.Entry.print ft e in
   str (Buffer.contents entry_buf)
 
 let pr_registered_grammar name =
@@ -55,7 +55,7 @@ let pr_registered_grammar name =
   | [] -> user_err Pp.(str "Unknown or unprintable grammar entry.")
   | entries ->
     let pr_one (Pcoq.AnyEntry e) =
-      str "Entry " ++ str (Pcoq.G.Entry.name e) ++ str " is" ++ fnl () ++
+      str "Entry " ++ str (Pcoq.Entry.name e) ++ str " is" ++ fnl () ++
       pr_entry e
     in
     prlist pr_one entries
diff --git a/vernac/proof_using.ml b/vernac/proof_using.ml
index 8d0dcbf0fe..2130a398e9 100644
--- a/vernac/proof_using.ml
+++ b/vernac/proof_using.ml
@@ -169,7 +169,7 @@ let suggest_variable env id =
 let value = ref None
 
 let using_to_string us = Pp.string_of_ppcmds (Ppvernac.pr_using us)
-let using_from_string us = Pcoq.G.Entry.parse G_vernac.section_subset_expr (Pcoq.G.Parsable.make (Stream.of_string us))
+let using_from_string us = Pcoq.Entry.parse G_vernac.section_subset_expr (Pcoq.Parsable.make (Stream.of_string us))
 
 let proof_using_opt_name = ["Default";"Proof";"Using"]
 let () =
diff --git a/vernac/pvernac.ml b/vernac/pvernac.ml
index 26364ed075..f4cb1adfe8 100644
--- a/vernac/pvernac.ml
+++ b/vernac/pvernac.ml
@@ -54,10 +54,10 @@ module Vernac_ =
       let act_vernac v loc = Some v in
       let act_eoi _ loc = None in
       let rule = [
-        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);
+        Pcoq.(Production.make (Rule.next Rule.stop (Symbol.token Tok.PEOI)) act_eoi);
+        Pcoq.(Production.make (Rule.next Rule.stop (Symbol.nterm vernac_control)) act_vernac);
       ] in
-      Pcoq.(grammar_extend main_entry {G.pos=None; data=[None, None, rule]})
+      Pcoq.(grammar_extend main_entry {pos=None; data=[None, None, rule]})
 
     let select_tactic_entry spec =
       match spec with
@@ -65,8 +65,8 @@ module Vernac_ =
       | Some ename -> find_proof_mode ename
 
     let command_entry =
-      Pcoq.G.Entry.of_parser "command_entry"
-        (fun _ strm -> Pcoq.G.Entry.parse_token_stream (select_tactic_entry !command_entry_ref) strm)
+      Pcoq.Entry.of_parser "command_entry"
+        (fun _ strm -> Pcoq.Entry.parse_token_stream (select_tactic_entry !command_entry_ref) strm)
 
   end
 
diff --git a/vernac/vernacextend.ml b/vernac/vernacextend.ml
index 4008c3d799..1920c276af 100644
--- a/vernac/vernacextend.ml
+++ b/vernac/vernacextend.ml
@@ -166,15 +166,15 @@ let rec untype_command : type r s. (r, s) ty_sig -> r -> plugin_args -> vernac_c
     | Some Refl -> untype_command ty (f v) args
   end
 
-let rec untype_user_symbol : type s a b c. (a, b, c) Extend.ty_user_symbol -> (s, Gramlib.Grammar.norec, a) Pcoq.G.Symbol.t =
+let rec untype_user_symbol : type s a b c. (a, b, c) Extend.ty_user_symbol -> (s, Gramlib.Grammar.norec, a) Pcoq.Symbol.t =
   let open Extend in function
-  | TUlist1 l -> Pcoq.G.Symbol.list1 (untype_user_symbol l)
-  | TUlist1sep (l, s) -> Pcoq.G.Symbol.list1sep (untype_user_symbol l) (Pcoq.G.Symbol.token (CLexer.terminal s)) false
-  | TUlist0 l -> Pcoq.G.Symbol.list0 (untype_user_symbol l)
-  | TUlist0sep (l, s) -> Pcoq.G.Symbol.list0sep (untype_user_symbol l) (Pcoq.G.Symbol.token (CLexer.terminal s)) false
-  | TUopt o -> Pcoq.G.Symbol.opt (untype_user_symbol o)
-  | TUentry a -> Pcoq.G.Symbol.nterm (Pcoq.genarg_grammar (Genarg.ExtraArg a))
-  | TUentryl (a, i) -> Pcoq.G.Symbol.nterml (Pcoq.genarg_grammar (Genarg.ExtraArg a)) (string_of_int i)
+  | TUlist1 l -> Pcoq.Symbol.list1 (untype_user_symbol l)
+  | TUlist1sep (l, s) -> Pcoq.Symbol.list1sep (untype_user_symbol l) (Pcoq.Symbol.token (CLexer.terminal s)) false
+  | TUlist0 l -> Pcoq.Symbol.list0 (untype_user_symbol l)
+  | TUlist0sep (l, s) -> Pcoq.Symbol.list0sep (untype_user_symbol l) (Pcoq.Symbol.token (CLexer.terminal s)) false
+  | TUopt o -> Pcoq.Symbol.opt (untype_user_symbol o)
+  | TUentry a -> Pcoq.Symbol.nterm (Pcoq.genarg_grammar (Genarg.ExtraArg a))
+  | TUentryl (a, i) -> Pcoq.Symbol.nterml (Pcoq.genarg_grammar (Genarg.ExtraArg a)) (string_of_int i)
 
 let rec untype_grammar : type r s. (r, s) ty_sig -> 'a Egramml.grammar_prod_item list = function
 | TyNil -> []
@@ -193,7 +193,7 @@ let vernac_extend ~command ?classifier ?entry ext =
     | None ->
       let e = match entry with
       | None -> "COMMAND"
-      | Some e -> Pcoq.G.Entry.name e
+      | Some e -> Pcoq.Entry.name e
       in
       let msg = Printf.sprintf "\
         Vernac entry \"%s\" misses a classifier. \
@@ -229,7 +229,7 @@ let vernac_extend ~command ?classifier ?entry ext =
 
 type 'a argument_rule =
 | Arg_alias of 'a Pcoq.Entry.t
-| Arg_rules of 'a Pcoq.G.Production.t list
+| Arg_rules of 'a Pcoq.Production.t list
 
 type 'a vernac_argument = {
   arg_printer : Environ.env -> Evd.evar_map -> 'a -> Pp.t;
@@ -244,7 +244,7 @@ let vernac_argument_extend ~name arg =
     e
   | Arg_rules rules ->
     let e = Pcoq.create_generic_entry Pcoq.utactic name (Genarg.rawwit wit) in
-    let () = Pcoq.grammar_extend e {Pcoq.G.pos=None; data=[(None, None, rules)]} in
+    let () = Pcoq.grammar_extend e {Pcoq.pos=None; data=[(None, None, rules)]} in
     e
   in
   let pr = arg.arg_printer in
diff --git a/vernac/vernacextend.mli b/vernac/vernacextend.mli
index 4d9537b6ff..0d0ebc1086 100644
--- a/vernac/vernacextend.mli
+++ b/vernac/vernacextend.mli
@@ -111,7 +111,7 @@ type 'a argument_rule =
 | Arg_alias of 'a Pcoq.Entry.t
   (** This is used because CAMLP5 parser can be dumb about rule factorization,
       which sometimes requires two entries to be the same. *)
-| Arg_rules of 'a Pcoq.G.Production.t list
+| Arg_rules of 'a Pcoq.Production.t list
   (** There is a discrepancy here as we use directly extension rules and thus
     entries instead of ty_user_symbol and thus arguments as roots. *)
 
diff --git a/vernac/vernacinterp.ml b/vernac/vernacinterp.ml
index 6b7b2c2691..15a19c06c2 100644
--- a/vernac/vernacinterp.ml
+++ b/vernac/vernacinterp.ml
@@ -183,12 +183,12 @@ and vernac_load ~verbosely fname =
   let input =
     let longfname = Loadpath.locate_file fname in
     let in_chan = Util.open_utf8_file_in longfname in
-    Pcoq.G.Parsable.make ~loc:(Loc.initial (Loc.InFile longfname)) (Stream.of_channel in_chan) in
+    Pcoq.Parsable.make ~loc:(Loc.initial (Loc.InFile longfname)) (Stream.of_channel in_chan) in
   (* Parsing loop *)
   let v_mod = if verbosely then Flags.verbosely else Flags.silently in
   let parse_sentence proof_mode = Flags.with_option Flags.we_are_parsing
       (fun po ->
-         match Pcoq.G.Entry.parse (Pvernac.main_entry proof_mode) po with
+         match Pcoq.Entry.parse (Pvernac.main_entry proof_mode) po with
          | Some x -> x
          | None -> raise End_of_input) in
   let rec load_loop ~stack =
diff --git a/vernac/vernacstate.ml b/vernac/vernacstate.ml
index 49486b889d..6846826bfa 100644
--- a/vernac/vernacstate.ml
+++ b/vernac/vernacstate.ml
@@ -19,7 +19,7 @@ module Parser = struct
   let parse ps entry pa =
     Pcoq.unfreeze ps;
     Flags.with_option Flags.we_are_parsing
-      (fun () -> Pcoq.G.Entry.parse entry pa)
+      (fun () -> Pcoq.Entry.parse entry pa)
       ()
 
 end
diff --git a/vernac/vernacstate.mli b/vernac/vernacstate.mli
index ed1b76b618..7607f8373a 100644
--- a/vernac/vernacstate.mli
+++ b/vernac/vernacstate.mli
@@ -14,7 +14,7 @@ module Parser : sig
   val init : unit -> state
   val cur_state : unit -> state
 
-  val parse : state -> 'a Pcoq.Entry.t -> Pcoq.G.Parsable.t -> 'a
+  val parse : state -> 'a Pcoq.Entry.t -> Pcoq.Parsable.t -> 'a
 
 end