Merge PR #9051: Camlp5 safe API strikes back

23 files changed, 116 insertions, 169 deletions

diff --git a/coqpp/coqpp_main.ml b/coqpp/coqpp_main.ml
index 8da4c6db13..d52bd39d72 100644
--- a/coqpp/coqpp_main.ml
+++ b/coqpp/coqpp_main.ml
@@ -139,7 +139,7 @@ let print_local fmt ext =
   match locals with
   | [] -> ()
   | e :: locals ->
-    let mk_e fmt e = fprintf fmt "%s.Entry.create \"%s\"" ext.gramext_name e in
+    let mk_e fmt e = fprintf fmt "Pcoq.Entry.create \"%s\"" e in
     let () = fprintf fmt "@[<hv 2>let %s =@ @[%a@]@]@ " e mk_e e in
     let iter e = fprintf fmt "@[<hv 2>and %s =@ @[%a@]@]@ " e mk_e e in
     let () = List.iter iter locals in
@@ -277,16 +277,16 @@ let print_rule fmt r =
   let pr_prd fmt prd = print_list fmt print_prod prd in
   fprintf fmt "@[(%a,@ %a,@ %a)@]" pr_lvl r.grule_label pr_asc r.grule_assoc pr_prd (List.rev r.grule_prods)
 
-let print_entry fmt gram e =
+let print_entry fmt e =
   let print_position_opt fmt pos = print_opt fmt print_position pos in
   let print_rules fmt rules = print_list fmt print_rule rules in
-  fprintf fmt "let () =@ @[%s.gram_extend@ %s@ @[(%a, %a)@]@]@ in@ "
-    gram e.gentry_name print_position_opt e.gentry_pos print_rules e.gentry_rules
+  fprintf fmt "let () =@ @[Pcoq.grammar_extend@ %s@ None@ @[(%a, %a)@]@]@ in@ "
+    e.gentry_name print_position_opt e.gentry_pos print_rules e.gentry_rules
 
 let print_ast fmt ext =
   let () = fprintf fmt "let _ = @[" in
   let () = fprintf fmt "@[<v>%a@]" print_local ext in
-  let () = List.iter (fun e -> print_entry fmt ext.gramext_name e) ext.gramext_entries in
+  let () = List.iter (fun e -> print_entry fmt e) ext.gramext_entries in
   let () = fprintf fmt "()@]@\n" in
   ()
 
diff --git a/dev/ci/user-overlays/09051-ppedrot-camlp5-safe-api-strikes-back.sh b/dev/ci/user-overlays/09051-ppedrot-camlp5-safe-api-strikes-back.sh
new file mode 100644
index 0000000000..14e7c0d7f0
--- /dev/null
+++ b/dev/ci/user-overlays/09051-ppedrot-camlp5-safe-api-strikes-back.sh
@@ -0,0 +1,9 @@
+if [ "$CI_PULL_REQUEST" = "9051" ] || [ "$CI_BRANCH" = "camlp5-safe-api-strikes-back" ]; then
+
+    equations_CI_REF=camlp5-safe-api-strikes-back
+    equations_CI_GITURL=https://github.com/ppedrot/Coq-Equations
+
+    ltac2_CI_REF=camlp5-safe-api-strikes-back
+    ltac2_CI_GITURL=https://github.com/ppedrot/ltac2
+
+fi
diff --git a/gramlib/gramext.ml b/gramlib/gramext.ml
index 72468b540e..43a70ca13b 100644
--- a/gramlib/gramext.ml
+++ b/gramlib/gramext.ml
@@ -149,8 +149,6 @@ let srules rl =
   in
   Stree t
 
-external action : 'a -> g_action = "%identity"
-
 let is_level_labelled n lev =
   match lev.lname with
     Some n1 -> n = n1
diff --git a/gramlib/gramext.mli b/gramlib/gramext.mli
index e888508277..8361e21645 100644
--- a/gramlib/gramext.mli
+++ b/gramlib/gramext.mli
@@ -59,7 +59,6 @@ val levels_of_rules :
       list ->
     'te g_level list
 val srules : ('te g_symbol list * g_action) list -> 'te g_symbol
-external action : 'a -> g_action = "%identity"
 val eq_symbol : 'a g_symbol -> 'a g_symbol -> bool
 
 val delete_rule_in_level_list :
diff --git a/gramlib/grammar.ml b/gramlib/grammar.ml
index 1ce0136c1d..dfce26a33a 100644
--- a/gramlib/grammar.ml
+++ b/gramlib/grammar.ml
@@ -5,6 +5,8 @@
 open Gramext
 open Format
 
+external gramext_action : 'a -> g_action = "%identity"
+
 let rec flatten_tree =
   function
     DeadEnd -> []
@@ -350,7 +352,7 @@ let top_tree entry =
   | LocAct (_, _) | DeadEnd -> raise Stream.Failure
 
 let skip_if_empty bp p strm =
-  if Stream.count strm == bp then Gramext.action (fun a -> p strm)
+  if Stream.count strm == bp then gramext_action (fun a -> p strm)
   else raise Stream.Failure
 
 let continue entry bp a s son p1 (strm__ : _ Stream.t) =
@@ -359,7 +361,7 @@ let continue entry bp a s son p1 (strm__ : _ Stream.t) =
     try p1 strm__ with
       Stream.Failure -> raise (Stream.Error (tree_failed entry a s son))
   in
-  Gramext.action (fun _ -> app act a)
+  gramext_action (fun _ -> app act a)
 
 let do_recover parser_of_tree entry nlevn alevn bp a s son
     (strm__ : _ Stream.t) =
@@ -861,7 +863,6 @@ module type S =
         val of_parser : string -> (te Stream.t -> 'a) -> 'a e
         val parse_token_stream : 'a e -> te Stream.t -> 'a
         val print : Format.formatter -> 'a e -> unit
-        external obj : 'a e -> te Gramext.g_entry = "%identity"
       end
     type ('self, 'a) ty_symbol
     type ('self, 'f, 'r) ty_rule
@@ -891,18 +892,11 @@ module type S =
         val gram_reinit : te Plexing.lexer -> unit
         val clear_entry : 'a Entry.e -> unit
       end
-    val extend :
-      'a Entry.e -> Gramext.position option ->
-        (string option * Gramext.g_assoc option *
-           (te Gramext.g_symbol list * Gramext.g_action) list)
-          list ->
-        unit
     val safe_extend :
       'a Entry.e -> Gramext.position option ->
         (string option * Gramext.g_assoc option * 'a ty_production list)
           list ->
         unit
-    val delete_rule : 'a Entry.e -> te Gramext.g_symbol list -> unit
     val safe_delete_rule : 'a Entry.e -> ('a, 'r, 'f) ty_rule -> unit
   end
 
diff --git a/gramlib/grammar.mli b/gramlib/grammar.mli
index 1c5fcb7bbf..1e14e557bc 100644
--- a/gramlib/grammar.mli
+++ b/gramlib/grammar.mli
@@ -35,7 +35,6 @@ module type S =
         val of_parser : string -> (te Stream.t -> 'a) -> 'a e
         val parse_token_stream : 'a e -> te Stream.t -> 'a
         val print : Format.formatter -> 'a e -> unit
-        external obj : 'a e -> te Gramext.g_entry = "%identity"
       end
     type ('self, 'a) ty_symbol
     type ('self, 'f, 'r) ty_rule
@@ -66,18 +65,11 @@ module type S =
         val gram_reinit : te Plexing.lexer -> unit
         val clear_entry : 'a Entry.e -> unit
       end
-    val extend :
-      'a Entry.e -> Gramext.position option ->
-        (string option * Gramext.g_assoc option *
-           (te Gramext.g_symbol list * Gramext.g_action) list)
-          list ->
-        unit
     val safe_extend :
       'a Entry.e -> Gramext.position option ->
         (string option * Gramext.g_assoc option * 'a ty_production list)
           list ->
         unit
-    val delete_rule : 'a Entry.e -> te Gramext.g_symbol list -> unit
     val safe_delete_rule : 'a Entry.e -> ('a, 'f, 'r) ty_rule -> unit
   end
    (** Signature type of the functor [Grammar.GMake]. The types and
diff --git a/parsing/g_constr.mlg b/parsing/g_constr.mlg
index e25f7aa54f..b3ae24e941 100644
--- a/parsing/g_constr.mlg
+++ b/parsing/g_constr.mlg
@@ -81,7 +81,7 @@ let err () = raise Stream.Failure
 (* Hack to parse "(x:=t)" as an explicit argument without conflicts with the *)
 (* admissible notation "(x t)" *)
 let lpar_id_coloneq =
-  Gram.Entry.of_parser "test_lpar_id_coloneq"
+  Pcoq.Entry.of_parser "test_lpar_id_coloneq"
     (fun strm ->
       match stream_nth 0 strm with
         | KEYWORD "(" ->
@@ -96,7 +96,7 @@ let lpar_id_coloneq =
         | _ -> err ())
 
 let impl_ident_head =
-  Gram.Entry.of_parser "impl_ident_head"
+  Pcoq.Entry.of_parser "impl_ident_head"
     (fun strm ->
       match stream_nth 0 strm with
 	| KEYWORD "{" ->
@@ -109,7 +109,7 @@ let impl_ident_head =
 	| _ -> err ())
 
 let name_colon =
-  Gram.Entry.of_parser "name_colon"
+  Pcoq.Entry.of_parser "name_colon"
     (fun strm ->
       match stream_nth 0 strm with
 	| IDENT s ->
diff --git a/parsing/g_prim.mlg b/parsing/g_prim.mlg
index dfb788907e..6247a12640 100644
--- a/parsing/g_prim.mlg
+++ b/parsing/g_prim.mlg
@@ -13,7 +13,6 @@
 open Names
 open Libnames
 
-open Pcoq
 open Pcoq.Prim
 
 let prim_kw = ["{"; "}"; "["; "]"; "("; ")"; "'"]
diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml
index 445338b786..170df6ad09 100644
--- a/parsing/pcoq.ml
+++ b/parsing/pcoq.ml
@@ -14,7 +14,6 @@ open Extend
 open Genarg
 open Gramlib
 
-let curry f x y = f (x, y)
 let uncurry f (x,y) = f x y
 
 (** Location Utils  *)
@@ -84,13 +83,9 @@ module type S =
   *)
 
   type 'a entry = 'a Entry.e
-  type internal_entry = Tok.t Gramext.g_entry
-  type symbol = Tok.t Gramext.g_symbol
-  type action = Gramext.g_action
   type coq_parsable
 
   val coq_parsable : ?file:Loc.source -> char Stream.t -> coq_parsable
-  val action : 'a -> action
   val entry_create : string -> 'a entry
   val entry_parse : 'a entry -> coq_parsable -> 'a
 
@@ -101,9 +96,6 @@ end with type 'a Entry.e = 'a Grammar.GMake(CLexer).Entry.e = struct
   include Grammar.GMake(CLexer)
 
   type 'a entry = 'a Entry.e
-  type internal_entry = Tok.t Gramext.g_entry
-  type symbol = Tok.t Gramext.g_symbol
-  type action = Gramext.g_action
 
   type coq_parsable = parsable * CLexer.lexer_state ref
 
@@ -114,7 +106,6 @@ end with type 'a Entry.e = 'a Grammar.GMake(CLexer).Entry.e = struct
     state := CLexer.get_lexer_state ();
     (a,state)
 
-  let action = Gramext.action
   let entry_create = Entry.create
 
   let entry_parse e (p,state) =
@@ -149,6 +140,9 @@ struct
   let create = G.Entry.create
   let parse = G.entry_parse
   let print = G.Entry.print
+  let of_parser = G.Entry.of_parser
+  let name = G.Entry.name
+  let parse_token_stream = G.Entry.parse_token_stream
 
 end
 
@@ -167,16 +161,9 @@ let of_coq_position = function
 | Extend.Level s -> Gramext.Level s
 
 module Symbols : sig
-  val stoken : Tok.t -> G.symbol
-  val sself : G.symbol
-  val snext : G.symbol
-  val slist0 : G.symbol -> G.symbol
-  val slist0sep : G.symbol * G.symbol -> G.symbol
-  val slist1 : G.symbol -> G.symbol
-  val slist1sep : G.symbol * G.symbol -> G.symbol
-  val sopt : G.symbol -> G.symbol
-  val snterml : G.internal_entry * string -> G.symbol
-  val snterm : G.internal_entry -> G.symbol
+  val stoken : Tok.t -> ('s, string) G.ty_symbol
+  val slist0sep : ('s, 'a) G.ty_symbol -> ('s, 'b) G.ty_symbol -> ('s, 'a list) G.ty_symbol
+  val slist1sep : ('s, 'a) G.ty_symbol -> ('s, 'b) G.ty_symbol -> ('s, 'a list) G.ty_symbol
 end = struct
 
   let stoken tok =
@@ -191,19 +178,10 @@ end = struct
     | Tok.BULLET s -> "BULLET", s
     | Tok.EOI -> "EOI", ""
     in
-    Gramext.Stoken pattern
-
-     let slist0sep (x, y) = Gramext.Slist0sep (x, y, false)
-     let slist1sep (x, y) = Gramext.Slist1sep (x, y, false)
-
-  let snterml (x, y) = Gramext.Snterml (x, y)
-  let snterm x = Gramext.Snterm x
-  let sself = Gramext.Sself
-  let snext = Gramext.Snext
-  let slist0 x = Gramext.Slist0 x
-  let slist1 x = Gramext.Slist1 x
-  let sopt x = Gramext.Sopt x
+    G.s_token pattern
 
+  let slist0sep x y = G.s_list0sep x y false
+  let slist1sep x y = G.s_list1sep x y false
 end
 
 let camlp5_verbosity silent f x =
@@ -225,40 +203,41 @@ let camlp5_verbosity silent f x =
 
 (** Binding general entry keys to symbol *)
 
-let rec of_coq_action : type a r. (r, a, Loc.t -> r) Extend.rule -> a -> G.action = function
-| Stop -> fun f -> G.action (fun loc -> f (!@ loc))
-| Next (r, _) -> fun f -> G.action (fun x -> of_coq_action r (f x))
-
-let rec symbol_of_prod_entry_key : type s a. (s, a) symbol -> _ = function
-  | Atoken t -> Symbols.stoken t
-  | Alist1 s -> Symbols.slist1 (symbol_of_prod_entry_key s)
-  | Alist1sep (s,sep) ->
-      Symbols.slist1sep (symbol_of_prod_entry_key s, symbol_of_prod_entry_key sep)
-  | Alist0 s -> Symbols.slist0 (symbol_of_prod_entry_key s)
-  | Alist0sep (s,sep) ->
-      Symbols.slist0sep (symbol_of_prod_entry_key s, symbol_of_prod_entry_key sep)
-  | Aopt s -> Symbols.sopt (symbol_of_prod_entry_key s)
-  | Aself -> Symbols.sself
-  | Anext -> Symbols.snext
-  | Aentry e ->
-    Symbols.snterm (G.Entry.obj e)
-  | Aentryl (e, n) ->
-    Symbols.snterml (G.Entry.obj e, n)
-  | Arules rs ->
-    Gramext.srules (List.map symbol_of_rules rs)
-
-and symbol_of_rule : type s a r. (s, a, r) Extend.rule -> _ = function
-| Stop -> fun accu -> accu
-| Next (r, s) -> fun accu -> symbol_of_rule r (symbol_of_prod_entry_key s :: accu)
-
-and symbol_of_rules : type a. a Extend.rules -> _ = function
+type ('s, 'a, 'r) casted_rule = Casted : ('s, 'b, 'r) G.ty_rule * ('a -> 'b) -> ('s, 'a, 'r) casted_rule
+
+let rec symbol_of_prod_entry_key : type s a. (s, a) symbol -> (s, a) G.ty_symbol = function
+| Atoken t -> Symbols.stoken t
+| Alist1 s -> G.s_list1 (symbol_of_prod_entry_key s)
+| Alist1sep (s,sep) ->
+    Symbols.slist1sep (symbol_of_prod_entry_key s) (symbol_of_prod_entry_key sep)
+| Alist0 s -> G.s_list0 (symbol_of_prod_entry_key s)
+| Alist0sep (s,sep) ->
+    Symbols.slist0sep (symbol_of_prod_entry_key s) (symbol_of_prod_entry_key sep)
+| Aopt s -> G.s_opt (symbol_of_prod_entry_key s)
+| Aself -> G.s_self
+| Anext -> G.s_next
+| Aentry e -> G.s_nterm e
+| Aentryl (e, n) -> G.s_nterml e n
+| Arules rs -> G.s_rules (List.map symbol_of_rules rs)
+
+and symbol_of_rule : type s a r. (s, a, Loc.t -> r) Extend.rule -> (s, a, Ploc.t -> r) casted_rule = function
+| Stop -> Casted (G.r_stop, fun act loc -> act (!@loc))
+| Next (r, s) ->
+  let Casted (r, cast) = symbol_of_rule r in
+  Casted (G.r_next r (symbol_of_prod_entry_key s), (fun act x -> cast (act x)))
+
+and symbol_of_rules : type a. a Extend.rules -> a G.ty_production = function
 | Rules (r, act) ->
-  let symb = symbol_of_rule r.norec_rule [] in
-  let act = of_coq_action r.norec_rule act in
-  (symb, act)
+  let Casted (symb, cast) = symbol_of_rule r.norec_rule in
+  G.production (symb, cast act)
+
+(** FIXME: This is a hack around a deficient camlp5 API *)
+type 'a any_production = AnyProduction : ('a, 'f, Ploc.t -> 'a) G.ty_rule * 'f -> 'a any_production
 
-let of_coq_production_rule : type a. a Extend.production_rule -> _ = function
-| Rule (toks, act) -> (symbol_of_rule toks [], of_coq_action toks act)
+let of_coq_production_rule : type a. a Extend.production_rule -> a any_production = function
+| Rule (toks, act) ->
+  let Casted (symb, cast) = symbol_of_rule toks in
+  AnyProduction (symb, cast act)
 
 let of_coq_single_extend_statement (lvl, assoc, rule) =
   (lvl, Option.map of_coq_assoc assoc, List.map of_coq_production_rule rule)
@@ -266,6 +245,13 @@ let of_coq_single_extend_statement (lvl, assoc, rule) =
 let of_coq_extend_statement (pos, st) =
   (Option.map of_coq_position pos, List.map of_coq_single_extend_statement st)
 
+let fix_extend_statement (pos, st) =
+  let fix_single_extend_statement (lvl, assoc, rules) =
+    let fix_production_rule (AnyProduction (s, act)) = G.production (s, act) in
+    (lvl, assoc, List.map fix_production_rule rules)
+  in
+  (pos, List.map fix_single_extend_statement st)
+
 (** Type of reinitialization data *)
 type gram_reinit = gram_assoc * gram_position
 
@@ -292,7 +278,7 @@ let camlp5_entries = ref EntryDataMap.empty
 let grammar_delete e reinit (pos,rls) =
   List.iter
     (fun (n,ass,lev) ->
-      List.iter (fun (pil,_) -> G.delete_rule e pil) (List.rev lev))
+      List.iter (fun (AnyProduction (pil,_)) -> G.safe_delete_rule e pil) (List.rev lev))
     (List.rev rls);
   match reinit with
   | Some (a,ext) ->
@@ -302,7 +288,7 @@ let grammar_delete e reinit (pos,rls) =
     | Some (Gramext.Level n) -> n
     | _ -> assert false
     in
-    (G.extend e) (Some ext) [Some lev,Some a,[]]
+    (G.safe_extend e) (Some ext) [Some lev,Some a,[]]
   | None -> ()
 
 (** Extension *)
@@ -310,13 +296,15 @@ let grammar_delete e reinit (pos,rls) =
 let grammar_extend e reinit ext =
   let ext = of_coq_extend_statement ext in
   let undo () = grammar_delete e reinit ext in
-  let redo () = camlp5_verbosity false (uncurry (G.extend e)) ext in
+  let ext = fix_extend_statement ext in
+  let redo () = camlp5_verbosity false (uncurry (G.safe_extend e)) ext in
   camlp5_state := ByEXTEND (undo, redo) :: !camlp5_state;
   redo ()
 
 let grammar_extend_sync e reinit ext =
   camlp5_state := ByGrammar (ExtendRule (e, reinit, ext)) :: !camlp5_state;
-  camlp5_verbosity false (uncurry (G.extend e)) (of_coq_extend_statement ext)
+  let ext = fix_extend_statement (of_coq_extend_statement ext) in
+  camlp5_verbosity false (uncurry (G.safe_extend e)) ext
 
 (** The apparent parser of Coq; encapsulate G to keep track
     of the extensions. *)
@@ -324,25 +312,6 @@ let grammar_extend_sync e reinit ext =
 module Gram =
   struct
     include G
-    let extend e =
-      curry
-    (fun ext ->
-      camlp5_state :=
-        (ByEXTEND ((fun () -> grammar_delete e None ext),
-           (fun () -> uncurry (G.extend e) ext)))
-      :: !camlp5_state;
-      uncurry (G.extend e) ext)
-    let delete_rule e pil =
-      (* spiwack: if you use load an ML module which contains GDELETE_RULE
-      in a section, God kills a kitty. As it would corrupt remove_grammars.
-          There does not seem to be a good way to undo a delete rule. As deleting
-      takes fewer arguments than extending. The production rule isn't returned
-      by delete_rule. If we could retrieve the necessary information, then
-      ByEXTEND provides just the framework we need to allow this in section.
-      I'm not entirely sure it makes sense, but at least it would be more correct.
-          *)
-      G.delete_rule e pil
-    let gram_extend e ext = grammar_extend e None ext
   end
 
 (** Remove extensions
@@ -381,16 +350,16 @@ let make_rule r = [None, None, r]
 
 let eoi_entry en =
   let e = Entry.create ((Gram.Entry.name en) ^ "_eoi") in
-  let symbs = [Symbols.snterm (Gram.Entry.obj en); Symbols.stoken Tok.EOI] in
-  let act = Gram.action (fun _ x loc -> x) in
-  uncurry (Gram.extend e) (None, make_rule [symbs, act]);
+  let symbs = G.r_next (G.r_next G.r_stop (G.s_nterm en)) (Symbols.stoken Tok.EOI) in
+  let act = fun _ x loc -> x in
+  Gram.safe_extend e None (make_rule [G.production (symbs, act)]);
   e
 
 let map_entry f en =
   let e = Entry.create ((Gram.Entry.name en) ^ "_map") in
-  let symbs = [Symbols.snterm (Gram.Entry.obj en)] in
-  let act = Gram.action (fun x loc -> f x) in
-  uncurry (Gram.extend e) (None, make_rule [symbs, act]);
+  let symbs = G.r_next G.r_stop (G.s_nterm en) in
+  let act = fun x loc -> f x in
+  Gram.safe_extend e None (make_rule [G.production (symbs, act)]);
   e
 
 (* Parse a string, does NOT check if the entire string was read
@@ -517,10 +486,10 @@ module Module =
   end
 
 let epsilon_value f e =
-  let r = Rule (Next (Stop, e), fun x _ -> f x) in
-  let ext = of_coq_extend_statement (None, [None, None, [r]]) in
+  let r = G.production (G.r_next G.r_stop (symbol_of_prod_entry_key e), (fun x _ -> f x)) in
+  let ext = [None, None, [r]] in
   let entry = Gram.entry_create "epsilon" in
-  let () = uncurry (G.extend entry) ext in
+  let () = G.safe_extend entry None ext in
   try Some (parse_string entry "") with _ -> None
 
 (** Synchronized grammar extensions *)
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index 593cf59341..e64c614149 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -17,17 +17,6 @@ open Gramlib
 
 (** The parser of Coq *)
 
-(** DO NOT USE EXTENSION FUNCTIONS IN THIS MODULE.
-    We only have it here to work with Camlp5. Handwritten grammar extensions
-    should use the safe [Pcoq.grammar_extend] function below. *)
-module Gram : sig
-
-  include Grammar.S with type te = Tok.t
-
-  val gram_extend : 'a Entry.e -> 'a Extend.extend_statement -> unit
-
-end with type 'a Entry.e = 'a Grammar.GMake(CLexer).Entry.e
-
 module Parsable :
 sig
   type t
@@ -41,6 +30,9 @@ module Entry : sig
   val create : string -> 'a t
   val parse : 'a t -> Parsable.t -> 'a
   val print : Format.formatter -> 'a t -> unit
+  val of_parser : string -> (Tok.t Stream.t -> 'a) -> 'a t
+  val parse_token_stream : 'a t -> Tok.t Stream.t -> 'a
+  val name : 'a t -> string
 end
 
 (** The parser of Coq is built from three kinds of rule declarations:
diff --git a/plugins/funind/g_indfun.mlg b/plugins/funind/g_indfun.mlg
index 7e707b423a..8f0440a2a4 100644
--- a/plugins/funind/g_indfun.mlg
+++ b/plugins/funind/g_indfun.mlg
@@ -145,7 +145,6 @@ END
 
 {
 
-module Gram = Pcoq.Gram
 module Vernac = Pvernac.Vernac_
 module Tactic = Pltac
 
diff --git a/plugins/ltac/extraargs.mlg b/plugins/ltac/extraargs.mlg
index c4c4e51ecc..156ee94a66 100644
--- a/plugins/ltac/extraargs.mlg
+++ b/plugins/ltac/extraargs.mlg
@@ -332,7 +332,7 @@ END
 
 let local_test_lpar_id_colon =
   let err () = raise Stream.Failure in
-  Pcoq.Gram.Entry.of_parser "lpar_id_colon"
+  Pcoq.Entry.of_parser "lpar_id_colon"
     (fun strm ->
       match Util.stream_nth 0 strm with
         | Tok.KEYWORD "(" ->
diff --git a/plugins/ltac/g_ltac.mlg b/plugins/ltac/g_ltac.mlg
index bd8a097154..338839ee96 100644
--- a/plugins/ltac/g_ltac.mlg
+++ b/plugins/ltac/g_ltac.mlg
@@ -70,7 +70,7 @@ let _ =
 
 (* Hack to parse "[ id" without dropping [ *)
 let test_bracket_ident =
-  Gram.Entry.of_parser "test_bracket_ident"
+  Pcoq.Entry.of_parser "test_bracket_ident"
     (fun strm ->
       match stream_nth 0 strm with
         | KEYWORD "[" ->
diff --git a/plugins/ltac/g_obligations.mlg b/plugins/ltac/g_obligations.mlg
index e29f78af5b..ef18dd6cdc 100644
--- a/plugins/ltac/g_obligations.mlg
+++ b/plugins/ltac/g_obligations.mlg
@@ -45,7 +45,6 @@ let with_tac f tac =
  * Subtac. These entries are named Subtac.<foo>
  *)
 
-module Gram = Pcoq.Gram
 module Tactic = Pltac
 
 open Pcoq
diff --git a/plugins/ltac/g_rewrite.mlg b/plugins/ltac/g_rewrite.mlg
index 2596bc22f2..f7375a0f01 100644
--- a/plugins/ltac/g_rewrite.mlg
+++ b/plugins/ltac/g_rewrite.mlg
@@ -226,8 +226,6 @@ let () =
   let raw_printer _ _ _ l = Pp.pr_non_empty_arg Ppconstr.pr_binders l in
   Pptactic.declare_extra_vernac_genarg_pprule wit_binders raw_printer
 
-open Pcoq
-
 }
 
 GRAMMAR EXTEND Gram
diff --git a/plugins/ltac/g_tactic.mlg b/plugins/ltac/g_tactic.mlg
index 0ce0fbd0cd..46ea3819ac 100644
--- a/plugins/ltac/g_tactic.mlg
+++ b/plugins/ltac/g_tactic.mlg
@@ -39,7 +39,7 @@ let err () = raise Stream.Failure
 (* Hack to parse "(x:=t)" as an explicit argument without conflicts with the *)
 (* admissible notation "(x t)" *)
 let test_lpar_id_coloneq =
-  Gram.Entry.of_parser "lpar_id_coloneq"
+  Pcoq.Entry.of_parser "lpar_id_coloneq"
     (fun strm ->
       match stream_nth 0 strm with
         | KEYWORD "(" ->
@@ -53,7 +53,7 @@ let test_lpar_id_coloneq =
 
 (* Hack to recognize "(x)" *)
 let test_lpar_id_rpar =
-  Gram.Entry.of_parser "lpar_id_coloneq"
+  Pcoq.Entry.of_parser "lpar_id_coloneq"
     (fun strm ->
       match stream_nth 0 strm with
         | KEYWORD "(" ->
@@ -67,7 +67,7 @@ let test_lpar_id_rpar =
 
 (* idem for (x:=t) and (1:=t) *)
 let test_lpar_idnum_coloneq =
-  Gram.Entry.of_parser "test_lpar_idnum_coloneq"
+  Pcoq.Entry.of_parser "test_lpar_idnum_coloneq"
     (fun strm ->
       match stream_nth 0 strm with
         | KEYWORD "(" ->
@@ -84,7 +84,7 @@ open Extraargs
 
 (* idem for (x1..xn:t) [n^2 complexity but exceptional use] *)
 let check_for_coloneq =
-  Gram.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
@@ -108,7 +108,7 @@ let check_for_coloneq =
       | _ -> err ())
 
 let lookup_at_as_comma =
-  Gram.Entry.of_parser "lookup_at_as_comma"
+  Pcoq.Entry.of_parser "lookup_at_as_comma"
     (fun strm ->
       match stream_nth 0 strm with
 	| KEYWORD (","|"at"|"as") -> ()
diff --git a/plugins/ssr/ssrparser.mlg b/plugins/ssr/ssrparser.mlg
index 7c91860228..2dff0cc84f 100644
--- a/plugins/ssr/ssrparser.mlg
+++ b/plugins/ssr/ssrparser.mlg
@@ -268,16 +268,16 @@ let negate_parser f x =
   | Some _ -> raise Stream.Failure 
 
 let test_not_ssrslashnum =
-  Pcoq.Gram.Entry.of_parser
+  Pcoq.Entry.of_parser
     "test_not_ssrslashnum" (negate_parser test_ssrslashnum10)
 let test_ssrslashnum00 =
-  Pcoq.Gram.Entry.of_parser "test_ssrslashnum01" test_ssrslashnum00
+  Pcoq.Entry.of_parser "test_ssrslashnum01" test_ssrslashnum00
 let test_ssrslashnum10 =
-  Pcoq.Gram.Entry.of_parser "test_ssrslashnum10" test_ssrslashnum10
+  Pcoq.Entry.of_parser "test_ssrslashnum10" test_ssrslashnum10
 let test_ssrslashnum11 =
-  Pcoq.Gram.Entry.of_parser "test_ssrslashnum11" test_ssrslashnum11
+  Pcoq.Entry.of_parser "test_ssrslashnum11" test_ssrslashnum11
 let test_ssrslashnum01 =
-  Pcoq.Gram.Entry.of_parser "test_ssrslashnum01" test_ssrslashnum01
+  Pcoq.Entry.of_parser "test_ssrslashnum01" test_ssrslashnum01
 
 }
 
@@ -470,7 +470,7 @@ let input_ssrtermkind strm = match Util.stream_nth 0 strm with
   | Tok.KEYWORD "@" -> xWithAt
   | _ -> xNoFlag
 
-let ssrtermkind = Pcoq.Gram.Entry.of_parser "ssrtermkind" input_ssrtermkind
+let ssrtermkind = Pcoq.Entry.of_parser "ssrtermkind" input_ssrtermkind
 
 (* New kinds of terms *)
 
@@ -481,7 +481,7 @@ let input_term_annotation strm =
   | Tok.KEYWORD "@" :: _ -> `At
   | _ -> `None
 let term_annotation =
-  Gram.Entry.of_parser "term_annotation" input_term_annotation
+  Pcoq.Entry.of_parser "term_annotation" input_term_annotation
 
 (* terms *)
 
@@ -800,7 +800,7 @@ let reject_ssrhid strm =
       | _ -> ())
   | _ -> ()
 
-let test_nohidden = Pcoq.Gram.Entry.of_parser "test_ssrhid" reject_ssrhid
+let test_nohidden = Pcoq.Entry.of_parser "test_ssrhid" reject_ssrhid
 
 }
 
@@ -961,7 +961,7 @@ let accept_ssrfwdid strm =
   | Tok.IDENT id -> accept_before_syms_or_any_id [":"; ":="; "("] strm
   | _ -> raise Stream.Failure
 
-let test_ssrfwdid = Gram.Entry.of_parser "test_ssrfwdid" accept_ssrfwdid
+let test_ssrfwdid = Pcoq.Entry.of_parser "test_ssrfwdid" accept_ssrfwdid
 
 }
 
@@ -1540,7 +1540,7 @@ let accept_ssrseqvar strm =
      accept_before_syms_or_ids ["["] ["first";"last"] strm
   | _ -> raise Stream.Failure
 
-let test_ssrseqvar = Gram.Entry.of_parser "test_ssrseqvar" accept_ssrseqvar
+let test_ssrseqvar = Pcoq.Entry.of_parser "test_ssrseqvar" accept_ssrseqvar
 
 let swaptacarg (loc, b) = (b, []), Some (TacId [])
 
@@ -1628,7 +1628,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 = Gram.Entry.of_parser "ssr_null" (fun _ -> ())
+let ssr_null_entry = Pcoq.Entry.of_parser "ssr_null" (fun _ -> ())
 
 }
 
@@ -1955,7 +1955,7 @@ let accept_ssreqid strm =
                       accept_before_syms [":"] strm
   | _ -> raise Stream.Failure
 
-let test_ssreqid = Gram.Entry.of_parser "test_ssreqid" accept_ssreqid
+let test_ssreqid = Pcoq.Entry.of_parser "test_ssreqid" accept_ssreqid
 
 }
 
@@ -2373,7 +2373,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
-  Gram.Entry.of_parser "test_ssr_rw_syntax" test
+  Pcoq.Entry.of_parser "test_ssr_rw_syntax" test
 
 }
 
@@ -2583,7 +2583,7 @@ let accept_idcomma strm =
   | Tok.IDENT _ | Tok.KEYWORD "_" -> accept_before_syms [","] strm
   | _ -> raise Stream.Failure
 
-let test_idcomma = Gram.Entry.of_parser "test_idcomma" accept_idcomma
+let test_idcomma = Pcoq.Entry.of_parser "test_idcomma" accept_idcomma
 
 }
 
diff --git a/plugins/ssrmatching/g_ssrmatching.mlg b/plugins/ssrmatching/g_ssrmatching.mlg
index 3f0794fdd4..4ddaeb49fd 100644
--- a/plugins/ssrmatching/g_ssrmatching.mlg
+++ b/plugins/ssrmatching/g_ssrmatching.mlg
@@ -11,7 +11,6 @@
 {
 
 open Ltac_plugin
-open Pcoq
 open Pcoq.Constr
 open Ssrmatching
 open Ssrmatching.Internal
@@ -69,7 +68,7 @@ let input_ssrtermkind strm = match Util.stream_nth 0 strm with
   | Tok.KEYWORD "(" -> '('
   | Tok.KEYWORD "@" -> '@'
   | _ -> ' '
-let ssrtermkind = Pcoq.Gram.Entry.of_parser "ssrtermkind" input_ssrtermkind
+let ssrtermkind = Pcoq.Entry.of_parser "ssrtermkind" input_ssrtermkind
 
 }
 
diff --git a/toplevel/coqloop.ml b/toplevel/coqloop.ml
index 6d5f049176..4630599229 100644
--- a/toplevel/coqloop.ml
+++ b/toplevel/coqloop.ml
@@ -245,7 +245,7 @@ let parse_to_dot =
     | Tok.EOI -> raise Stm.End_of_input
     | _ -> dot st
   in
-  Pcoq.Gram.Entry.of_parser "Coqtoplevel.dot" dot
+  Pcoq.Entry.of_parser "Coqtoplevel.dot" dot
 
 (* If an error occurred while parsing, we try to read the input until a dot
    token is encountered.
diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg
index 3cdf81ced0..e3f6a87541 100644
--- a/vernac/g_vernac.mlg
+++ b/vernac/g_vernac.mlg
@@ -474,7 +474,7 @@ END
 {
 
 let only_starredidentrefs =
-  Gram.Entry.of_parser "test_only_starredidentrefs"
+  Pcoq.Entry.of_parser "test_only_starredidentrefs"
     (fun strm ->
       let rec aux n =
       match Util.stream_nth n strm with
diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml
index 2e5e11bb09..5ab877fae2 100644
--- a/vernac/metasyntax.ml
+++ b/vernac/metasyntax.ml
@@ -58,7 +58,7 @@ let pr_registered_grammar name =
   | None -> user_err Pp.(str "Unknown or unprintable grammar entry.")
   | Some entries ->
     let pr_one (Pcoq.AnyEntry e) =
-      str "Entry " ++ str (Pcoq.Gram.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/pvernac.ml b/vernac/pvernac.ml
index 4761e4bbc2..f26e0d0885 100644
--- a/vernac/pvernac.ml
+++ b/vernac/pvernac.ml
@@ -41,8 +41,8 @@ module Vernac_ =
 
     let command_entry_ref = ref noedit_mode
     let command_entry =
-      Gram.Entry.of_parser "command_entry"
-        (fun strm -> Gram.Entry.parse_token_stream !command_entry_ref strm)
+      Pcoq.Entry.of_parser "command_entry"
+        (fun strm -> Pcoq.Entry.parse_token_stream !command_entry_ref strm)
 
   end
 
diff --git a/vernac/vernacextend.ml b/vernac/vernacextend.ml
index 3a321ecdb4..35f26cab4d 100644
--- a/vernac/vernacextend.ml
+++ b/vernac/vernacextend.ml
@@ -190,7 +190,7 @@ let vernac_extend ~command ?classifier ?entry ext =
     | None ->
       let e = match entry with
       | None -> "COMMAND"
-      | Some e -> Pcoq.Gram.Entry.name e
+      | Some e -> Pcoq.Entry.name e
       in
       let msg = Printf.sprintf "\
         Vernac entry \"%s\" misses a classifier. \