Merge PR #9064: [gramlib] Minor cleanups:

15 files changed, 137 insertions, 170 deletions

diff --git a/coqpp/coqpp_main.ml b/coqpp/coqpp_main.ml
index d52bd39d72..8d728b5b51 100644
--- a/coqpp/coqpp_main.ml
+++ b/coqpp/coqpp_main.ml
@@ -146,16 +146,16 @@ let print_local fmt ext =
     fprintf fmt "in@ "
 
 let print_position fmt pos = match pos with
-| First -> fprintf fmt "Extend.First"
-| Last -> fprintf fmt "Extend.Last"
-| Before s -> fprintf fmt "Extend.Before@ \"%s\"" s
-| After s -> fprintf fmt "Extend.After@ \"%s\"" s
-| Level s -> fprintf fmt "Extend.Level@ \"%s\"" s
+| First -> fprintf fmt "Gramlib.Gramext.First"
+| Last -> fprintf fmt "Gramlib.Gramext.Last"
+| Before s -> fprintf fmt "Gramlib.Gramext.Before@ \"%s\"" s
+| After s -> fprintf fmt "Gramlib.Gramext.After@ \"%s\"" s
+| Level s -> fprintf fmt "Gramlib.Gramext.Level@ \"%s\"" s
 
 let print_assoc fmt = function
-| LeftA -> fprintf fmt "Extend.LeftA"
-| RightA -> fprintf fmt "Extend.RightA"
-| NonA -> fprintf fmt "Extend.NonA"
+| LeftA -> fprintf fmt "Gramlib.Gramext.LeftA"
+| RightA -> fprintf fmt "Gramlib.Gramext.RightA"
+| NonA -> fprintf fmt "Gramlib.Gramext.NonA"
 
 let is_token s = match string_split s with
 | [s] -> is_uident s
diff --git a/gramlib/gramext.ml b/gramlib/gramext.ml
index 43a70ca13b..c35c4bd18e 100644
--- a/gramlib/gramext.ml
+++ b/gramlib/gramext.ml
@@ -55,8 +55,6 @@ type position =
   | Like of string
   | Level of string
 
-let warning_verbose = ref true
-
 let rec derive_eps =
   function
     Slist0 _ -> true
@@ -96,7 +94,7 @@ let is_before s1 s2 =
   | Stoken _, _ -> true
   | _ -> false
 
-let insert_tree entry_name gsymbols action tree =
+let insert_tree ~warning entry_name gsymbols action tree =
   let rec insert symbols tree =
     match symbols with
       s :: sl -> insert_in_tree s sl tree
@@ -105,14 +103,16 @@ let insert_tree entry_name gsymbols action tree =
           Node {node = s; son = son; brother = bro} ->
             Node {node = s; son = son; brother = insert [] bro}
         | LocAct (old_action, action_list) ->
-            if !warning_verbose then
-              begin
-                eprintf "<W> Grammar extension: ";
-                if entry_name <> "" then eprintf "in [%s], " entry_name;
-                eprintf "some rule has been masked\n";
-                flush stderr
-              end;
-            LocAct (action, old_action :: action_list)
+          begin match warning with
+            | None -> ()
+            | Some warn_fn ->
+              let msg =
+                "<W> Grammar extension: " ^
+                (if entry_name <> "" then "" else "in ["^entry_name^"%s], ") ^
+                "some rule has been masked" in
+              warn_fn msg
+          end;
+          LocAct (action, old_action :: action_list)
         | DeadEnd -> LocAct (action, [])
   and insert_in_tree s sl tree =
     match try_insert s sl tree with
@@ -141,10 +141,10 @@ let insert_tree entry_name gsymbols action tree =
   in
   insert gsymbols tree
 
-let srules rl =
+let srules ~warning rl =
   let t =
     List.fold_left
-      (fun tree (symbols, action) -> insert_tree "" symbols action tree)
+      (fun tree (symbols, action) -> insert_tree ~warning "" symbols action tree)
       DeadEnd rl
   in
   Stree t
@@ -175,15 +175,15 @@ and token_exists_in_symbol f =
   | Stree t -> token_exists_in_tree f t
   | Snterm _ | Snterml (_, _) | Snext | Sself -> false
 
-let insert_level entry_name e1 symbols action slev =
+let insert_level ~warning entry_name e1 symbols action slev =
   match e1 with
     true ->
       {assoc = slev.assoc; lname = slev.lname;
-       lsuffix = insert_tree entry_name symbols action slev.lsuffix;
+       lsuffix = insert_tree ~warning entry_name symbols action slev.lsuffix;
        lprefix = slev.lprefix}
   | false ->
       {assoc = slev.assoc; lname = slev.lname; lsuffix = slev.lsuffix;
-       lprefix = insert_tree entry_name symbols action slev.lprefix}
+       lprefix = insert_tree ~warning entry_name symbols action slev.lprefix}
 
 let empty_lev lname assoc =
   let assoc =
@@ -193,27 +193,33 @@ let empty_lev lname assoc =
   in
   {assoc = assoc; lname = lname; lsuffix = DeadEnd; lprefix = DeadEnd}
 
-let change_lev lev n lname assoc =
+let change_lev ~warning lev n lname assoc =
   let a =
     match assoc with
       None -> lev.assoc
     | Some a ->
-        if a <> lev.assoc && !warning_verbose then
-          begin
-            eprintf "<W> Changing associativity of level \"%s\"\n" n;
-            flush stderr
-          end;
+      if a <> lev.assoc then
+        begin
+          match warning with
+          | None -> ()
+          | Some warn_fn ->
+            warn_fn ("<W> Changing associativity of level \""^n^"\"")
+        end;
         a
   in
   begin match lname with
     Some n ->
-      if lname <> lev.lname && !warning_verbose then
-        begin eprintf "<W> Level label \"%s\" ignored\n" n; flush stderr end
+      if lname <> lev.lname then
+        begin match warning with
+          | None -> ()
+          | Some warn_fn ->
+            warn_fn ("<W> Level label \""^n^"\" ignored")
+        end;
   | None -> ()
   end;
   {assoc = a; lname = lev.lname; lsuffix = lev.lsuffix; lprefix = lev.lprefix}
 
-let get_level entry position levs =
+let get_level ~warning entry position levs =
   match position with
     Some First -> [], empty_lev, levs
   | Some Last -> levs, empty_lev, []
@@ -226,7 +232,7 @@ let get_level entry position levs =
             flush stderr;
             failwith "Grammar.extend"
         | lev :: levs ->
-            if is_level_labelled n lev then [], change_lev lev n, levs
+            if is_level_labelled n lev then [], change_lev ~warning lev n, levs
             else
               let (levs1, rlev, levs2) = get levs in lev :: levs1, rlev, levs2
       in
@@ -268,14 +274,14 @@ let get_level entry position levs =
             flush stderr;
             failwith "Grammar.extend"
         | lev :: levs ->
-            if token_exists_in_level f lev then [], change_lev lev n, levs
+            if token_exists_in_level f lev then [], change_lev ~warning lev n, levs
             else
               let (levs1, rlev, levs2) = get levs in lev :: levs1, rlev, levs2
       in
       get levs
   | None ->
       match levs with
-        lev :: levs -> [], change_lev lev "<top>", levs
+        lev :: levs -> [], change_lev ~warning lev "<top>", levs
       | [] -> [], empty_lev, []
 
 let rec check_gram entry =
@@ -347,7 +353,7 @@ let insert_tokens gram symbols =
   in
   List.iter insert symbols
 
-let levels_of_rules entry position rules =
+let levels_of_rules ~warning entry position rules =
   let elev =
     match entry.edesc with
       Dlevels elev -> elev
@@ -358,7 +364,7 @@ let levels_of_rules entry position rules =
   in
   if rules = [] then elev
   else
-    let (levs1, make_lev, levs2) = get_level entry position elev in
+    let (levs1, make_lev, levs2) = get_level ~warning entry position elev in
     let (levs, _) =
       List.fold_left
         (fun (levs, make_lev) (lname, assoc, level) ->
@@ -370,7 +376,7 @@ let levels_of_rules entry position rules =
                   List.iter (check_gram entry) symbols;
                   let (e1, symbols) = get_initial entry symbols in
                   insert_tokens entry.egram symbols;
-                  insert_level entry.ename e1 symbols action lev)
+                  insert_level ~warning entry.ename e1 symbols action lev)
                lev level
            in
            lev :: levs, empty_lev)
diff --git a/gramlib/gramext.mli b/gramlib/gramext.mli
index 8361e21645..ecb95ec61b 100644
--- a/gramlib/gramext.mli
+++ b/gramlib/gramext.mli
@@ -53,15 +53,14 @@ type position =
   | Like of string
   | Level of string
 
-val levels_of_rules :
+val levels_of_rules : warning:(string -> unit) option ->
   'te g_entry -> position option ->
     (string option * g_assoc option * ('te g_symbol list * g_action) list)
       list ->
     'te g_level list
-val srules : ('te g_symbol list * g_action) list -> 'te g_symbol
+
+val srules : warning:(string -> unit) option -> ('te g_symbol list * g_action) list -> 'te g_symbol
 val eq_symbol : 'a g_symbol -> 'a g_symbol -> bool
 
 val delete_rule_in_level_list :
   'te g_entry -> 'te g_symbol list -> 'te g_level list -> 'te g_level list
-
-val warning_verbose : bool ref
diff --git a/gramlib/grammar.ml b/gramlib/grammar.ml
index dfce26a33a..285c14ec62 100644
--- a/gramlib/grammar.ml
+++ b/gramlib/grammar.ml
@@ -755,9 +755,9 @@ let init_entry_functions entry =
        let f = continue_parser_of_entry entry in
        entry.econtinue <- f; f lev bp a strm)
 
-let extend_entry entry position rules =
+let extend_entry ~warning entry position rules =
   try
-    let elev = Gramext.levels_of_rules entry position rules in
+    let elev = Gramext.levels_of_rules ~warning entry position rules in
     entry.edesc <- Dlevels elev; init_entry_functions entry
   with Plexing.Error s ->
     Printf.eprintf "Lexer initialization error:\n- %s\n" s;
@@ -841,8 +841,6 @@ let clear_entry e =
     Dlevels _ -> e.edesc <- Dlevels []
   | Dparser _ -> ()
 
-let gram_reinit g glexer = Hashtbl.clear g.gtokens; g.glexer <- glexer
-
 (* Functorial interface *)
 
 module type GLexerType = sig type te val lexer : te Plexing.lexer end
@@ -881,7 +879,7 @@ module type S =
     val s_self : ('self, 'self) ty_symbol
     val s_next : ('self, 'self) ty_symbol
     val s_token : Plexing.pattern -> ('self, string) ty_symbol
-    val s_rules : 'a ty_production list -> ('self, 'a) ty_symbol
+    val s_rules : warning:(string -> unit) option -> 'a ty_production list -> ('self, 'a) ty_symbol
     val r_stop : ('self, 'r, 'r) ty_rule
     val r_next :
       ('self, 'a, 'r) ty_rule -> ('self, 'b) ty_symbol ->
@@ -889,10 +887,9 @@ module type S =
     val production : ('a, 'f, Ploc.t -> 'a) ty_rule * 'f -> 'a ty_production
     module Unsafe :
       sig
-        val gram_reinit : te Plexing.lexer -> unit
         val clear_entry : 'a Entry.e -> unit
       end
-    val safe_extend :
+    val safe_extend : warning:(string -> unit) option ->
       'a Entry.e -> Gramext.position option ->
         (string option * Gramext.g_assoc option * 'a ty_production list)
           list ->
@@ -945,7 +942,7 @@ module GMake (L : GLexerType) =
     let s_self = Sself
     let s_next = Snext
     let s_token tok = Stoken tok
-    let s_rules (t : Obj.t ty_production list) = Gramext.srules (Obj.magic t)
+    let s_rules ~warning (t : Obj.t ty_production list) = Gramext.srules ~warning (Obj.magic t)
     let r_stop = []
     let r_next r s = r @ [s]
     let production
@@ -953,15 +950,12 @@ module GMake (L : GLexerType) =
       Obj.magic p
     module Unsafe =
       struct
-        let gram_reinit = gram_reinit gram
         let clear_entry = clear_entry
       end
-    let extend = extend_entry
-    let safe_extend e pos
+    let safe_extend ~warning e pos
         (r :
          (string option * Gramext.g_assoc option * Obj.t ty_production list)
            list) =
-      extend e pos (Obj.magic r)
-    let delete_rule e r = delete_rule (Entry.obj e) r
-    let safe_delete_rule = delete_rule
+      extend_entry ~warning e pos (Obj.magic r)
+    let safe_delete_rule e r = delete_rule (Entry.obj e) r
   end
diff --git a/gramlib/grammar.mli b/gramlib/grammar.mli
index 1e14e557bc..0c585a7c0d 100644
--- a/gramlib/grammar.mli
+++ b/gramlib/grammar.mli
@@ -53,7 +53,7 @@ module type S =
     val s_self : ('self, 'self) ty_symbol
     val s_next : ('self, 'self) ty_symbol
     val s_token : Plexing.pattern -> ('self, string) ty_symbol
-    val s_rules : 'a ty_production list -> ('self, 'a) ty_symbol
+    val s_rules : warning:(string -> unit) option -> 'a ty_production list -> ('self, 'a) ty_symbol
     val r_stop : ('self, 'r, 'r) ty_rule
     val r_next :
       ('self, 'a, 'r) ty_rule -> ('self, 'b) ty_symbol ->
@@ -62,10 +62,9 @@ module type S =
 
     module Unsafe :
       sig
-        val gram_reinit : te Plexing.lexer -> unit
         val clear_entry : 'a Entry.e -> unit
       end
-    val safe_extend :
+    val safe_extend : warning:(string -> unit) option ->
       'a Entry.e -> Gramext.position option ->
         (string option * Gramext.g_assoc option * 'a ty_production list)
           list ->
diff --git a/parsing/extend.ml b/parsing/extend.ml
index 5caeab535a..050ed49622 100644
--- a/parsing/extend.ml
+++ b/parsing/extend.ml
@@ -14,17 +14,8 @@ type 'a entry = 'a Gramlib.Grammar.GMake(CLexer).Entry.e
 
 type side = Left | Right
 
-type gram_assoc = NonA | RightA | LeftA
-
-type gram_position =
-  | First
-  | Last
-  | Before of string
-  | After of string
-  | Level of string
-
 type production_position =
-  | BorderProd of side * gram_assoc option
+  | BorderProd of side * Gramlib.Gramext.g_assoc option
   | InternalProd
 
 type production_level =
@@ -116,11 +107,11 @@ type 'a production_rule =
 type 'a single_extend_statement =
   string option *
   (** Level *)
-  gram_assoc option *
+  Gramlib.Gramext.g_assoc option *
   (** Associativity *)
   'a production_rule list
   (** Symbol list with the interpretation function *)
 
 type 'a extend_statement =
-  gram_position option *
+  Gramlib.Gramext.position option *
   'a single_extend_statement list
diff --git a/parsing/notation_gram.ml b/parsing/notation_gram.ml
index d8c08803b6..fc5feba58b 100644
--- a/parsing/notation_gram.ml
+++ b/parsing/notation_gram.ml
@@ -32,7 +32,7 @@ type grammar_constr_prod_item =
 
 type one_notation_grammar = {
   notgram_level : level;
-  notgram_assoc : Extend.gram_assoc option;
+  notgram_assoc : Gramlib.Gramext.g_assoc option;
   notgram_notation : Constrexpr.notation;
   notgram_prods : grammar_constr_prod_item list list;
 }
diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml
index 170df6ad09..816a02a6aa 100644
--- a/parsing/pcoq.ml
+++ b/parsing/pcoq.ml
@@ -14,8 +14,6 @@ open Extend
 open Genarg
 open Gramlib
 
-let uncurry f (x,y) = f x y
-
 (** Location Utils  *)
 let ploc_file_of_coq_file = function
 | Loc.ToplevelInput -> ""
@@ -82,7 +80,6 @@ module type S =
   end
   *)
 
-  type 'a entry = 'a Entry.e
   type coq_parsable
 
   val coq_parsable : ?file:Loc.source -> char Stream.t -> coq_parsable
@@ -91,12 +88,10 @@ module type S =
 
   val comment_state : coq_parsable -> ((int * int) * string) list
 
-end with type 'a Entry.e = 'a Grammar.GMake(CLexer).Entry.e = struct
+end with type 'a Entry.e = 'a Extend.entry = struct
 
   include Grammar.GMake(CLexer)
 
-  type 'a entry = 'a Entry.e
-
   type coq_parsable = parsable * CLexer.lexer_state ref
 
   let coq_parsable ?(file=Loc.ToplevelInput) c =
@@ -146,20 +141,6 @@ struct
 
 end
 
-let warning_verbose = Gramext.warning_verbose
-
-let of_coq_assoc = function
-| Extend.RightA -> Gramext.RightA
-| Extend.LeftA -> Gramext.LeftA
-| Extend.NonA -> Gramext.NonA
-
-let of_coq_position = function
-| Extend.First -> Gramext.First
-| Extend.Last -> Gramext.Last
-| Extend.Before s -> Gramext.Before s
-| Extend.After s -> Gramext.After s
-| Extend.Level s -> Gramext.Level s
-
 module Symbols : sig
   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
@@ -184,12 +165,6 @@ end = struct
   let slist1sep x y = G.s_list1sep x y false
 end
 
-let camlp5_verbosity silent f x =
-  let a = !warning_verbose in
-  warning_verbose := silent;
-  f x;
-  warning_verbose := a
-
 (** Grammar extensions *)
 
 (** NB: [extend_statement =
@@ -218,7 +193,9 @@ let rec symbol_of_prod_entry_key : type s a. (s, a) symbol -> (s, a) G.ty_symbol
 | 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)
+| Arules rs ->
+  let warning msg = Feedback.msg_warning Pp.(str msg) in
+  G.s_rules ~warning:(Some warning) (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))
@@ -240,10 +217,10 @@ let of_coq_production_rule : type a. a Extend.production_rule -> a any_productio
   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)
+  (lvl, assoc, List.map of_coq_production_rule rule)
 
 let of_coq_extend_statement (pos, st) =
-  (Option.map of_coq_position pos, List.map of_coq_single_extend_statement st)
+  (pos, List.map of_coq_single_extend_statement st)
 
 let fix_extend_statement (pos, st) =
   let fix_single_extend_statement (lvl, assoc, rules) =
@@ -253,19 +230,19 @@ let fix_extend_statement (pos, st) =
   (pos, List.map fix_single_extend_statement st)
 
 (** Type of reinitialization data *)
-type gram_reinit = gram_assoc * gram_position
+type gram_reinit = Gramlib.Gramext.g_assoc * Gramlib.Gramext.position
 
 type extend_rule =
-| ExtendRule : 'a G.entry * gram_reinit option * 'a extend_statement -> extend_rule
+| ExtendRule : 'a G.Entry.e * gram_reinit option * 'a extend_statement -> extend_rule
 
 module EntryCommand = Dyn.Make ()
-module EntryData = struct type _ t = Ex : 'b G.entry String.Map.t -> ('a * 'b) t end
+module EntryData = struct type _ t = Ex : 'b G.Entry.e String.Map.t -> ('a * 'b) t end
 module EntryDataMap = EntryCommand.Map(EntryData)
 
 type ext_kind =
   | ByGrammar of extend_rule
   | ByEXTEND of (unit -> unit) * (unit -> unit)
-  | ByEntry : ('a * 'b) EntryCommand.tag * string * 'b G.entry -> ext_kind
+  | ByEntry : ('a * 'b) EntryCommand.tag * string * 'b G.Entry.e -> ext_kind
 
 (** The list of extensions *)
 
@@ -282,13 +259,12 @@ let grammar_delete e reinit (pos,rls) =
     (List.rev rls);
   match reinit with
   | Some (a,ext) ->
-    let a = of_coq_assoc a in
-    let ext = of_coq_position ext in
     let lev = match pos with
     | Some (Gramext.Level n) -> n
     | _ -> assert false
     in
-    (G.safe_extend e) (Some ext) [Some lev,Some a,[]]
+    let warning msg = Feedback.msg_warning Pp.(str msg) in
+    (G.safe_extend ~warning:(Some warning) e) (Some ext) [Some lev,Some a,[]]
   | None -> ()
 
 (** Extension *)
@@ -296,15 +272,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 ext = fix_extend_statement ext in
-  let redo () = camlp5_verbosity false (uncurry (G.safe_extend e)) ext in
+  let pos, ext = fix_extend_statement ext in
+  let redo () = G.safe_extend ~warning:None e pos 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;
-  let ext = fix_extend_statement (of_coq_extend_statement ext) in
-  camlp5_verbosity false (uncurry (G.safe_extend e)) ext
+  let pos, ext = fix_extend_statement (of_coq_extend_statement ext) in
+  G.safe_extend ~warning:None e pos ext
 
 (** The apparent parser of Coq; encapsulate G to keep track
     of the extensions. *)
@@ -352,14 +328,16 @@ let eoi_entry en =
   let e = Entry.create ((Gram.Entry.name en) ^ "_eoi") in
   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)]);
+  let warning msg = Feedback.msg_warning Pp.(str msg) in
+  Gram.safe_extend ~warning:(Some warning) 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 = 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)]);
+  let warning msg = Feedback.msg_warning Pp.(str msg) in
+  Gram.safe_extend ~warning:(Some warning) e None (make_rule [G.production (symbs, act)]);
   e
 
 (* Parse a string, does NOT check if the entire string was read
@@ -489,7 +467,8 @@ let epsilon_value f e =
   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 () = G.safe_extend entry None ext in
+  let warning msg = Feedback.msg_warning Pp.(str msg) in
+  let () = G.safe_extend ~warning:(Some warning) entry None ext in
   try Some (parse_string entry "") with _ -> None
 
 (** Synchronized grammar extensions *)
@@ -542,7 +521,7 @@ let extend_grammar_command tag g =
   let nb = List.length rules in
   grammar_stack := (GramExt (nb, GrammarCommand.Dyn (tag, g)), st) :: !grammar_stack
 
-let extend_entry_command (type a) (type b) (tag : (a, b) entry_command) (g : a) : b Gram.entry list =
+let extend_entry_command (type a) (type b) (tag : (a, b) entry_command) (g : a) : b Gram.Entry.e list =
   let EntryInterp.Ex modify = EntryInterpMap.find tag !entry_interp in
   let grammar_state = match !grammar_stack with
   | [] -> GramState.empty
@@ -574,7 +553,7 @@ let extend_dyn_grammar (e, _) = match e with
 
 (** Registering extra grammar *)
 
-type any_entry = AnyEntry : 'a Gram.entry -> any_entry
+type any_entry = AnyEntry : 'a Gram.Entry.e -> any_entry
 
 let grammar_names : any_entry list String.Map.t ref = ref String.Map.empty
 
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index e64c614149..69ba57d516 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -26,7 +26,7 @@ sig
 end
 
 module Entry : sig
-  type 'a t = 'a Grammar.GMake(CLexer).Entry.e
+  type 'a t = 'a Extend.entry
   val create : string -> 'a t
   val parse : 'a t -> Parsable.t -> 'a
   val print : Format.formatter -> 'a t -> unit
@@ -110,10 +110,6 @@ end
 
 *)
 
-(** Temporarily activate camlp5 verbosity *)
-
-val camlp5_verbosity : bool -> ('a -> unit) -> 'a -> unit
-
 (** Parse a string *)
 
 val parse_string : 'a Entry.t -> string -> 'a
@@ -202,7 +198,7 @@ val epsilon_value : ('a -> 'self) -> ('self, 'a) Extend.symbol -> 'self option
 
 (** {5 Extending the parser without synchronization} *)
 
-type gram_reinit = gram_assoc * gram_position
+type gram_reinit = Gramlib.Gramext.g_assoc * Gramlib.Gramext.position
 (** Type of reinitialization data *)
 
 val grammar_extend : 'a Entry.t -> gram_reinit option ->
diff --git a/plugins/ltac/tacentries.ml b/plugins/ltac/tacentries.ml
index ac2d88dec2..2aee809eb6 100644
--- a/plugins/ltac/tacentries.ml
+++ b/plugins/ltac/tacentries.ml
@@ -119,7 +119,7 @@ let get_tactic_entry n =
   else if Int.equal n 5 then
     Pltac.binder_tactic, None
   else if 1<=n && n<5 then
-    Pltac.tactic_expr, Some (Extend.Level (string_of_int n))
+    Pltac.tactic_expr, Some (Gramlib.Gramext.Level (string_of_int n))
   else
     user_err Pp.(str ("Invalid Tactic Notation level: "^(string_of_int n)^"."))
 
diff --git a/vernac/egramcoq.ml b/vernac/egramcoq.ml
index 16101396cf..43abc0a200 100644
--- a/vernac/egramcoq.ml
+++ b/vernac/egramcoq.ml
@@ -33,24 +33,24 @@ open Pcoq
 let constr_level = string_of_int
 
 let default_levels =
-  [200,Extend.RightA,false;
-   100,Extend.RightA,false;
-   99,Extend.RightA,true;
-   90,Extend.RightA,true;
-   10,Extend.LeftA,false;
-   9,Extend.RightA,false;
-   8,Extend.RightA,true;
-   1,Extend.LeftA,false;
-   0,Extend.RightA,false]
+  [200,Gramlib.Gramext.RightA,false;
+   100,Gramlib.Gramext.RightA,false;
+   99,Gramlib.Gramext.RightA,true;
+   90,Gramlib.Gramext.RightA,true;
+   10,Gramlib.Gramext.LeftA,false;
+   9,Gramlib.Gramext.RightA,false;
+   8,Gramlib.Gramext.RightA,true;
+   1,Gramlib.Gramext.LeftA,false;
+   0,Gramlib.Gramext.RightA,false]
 
 let default_pattern_levels =
-  [200,Extend.RightA,true;
-   100,Extend.RightA,false;
-   99,Extend.RightA,true;
-   90,Extend.RightA,true;
-   10,Extend.LeftA,false;
-   1,Extend.LeftA,false;
-   0,Extend.RightA,false]
+  [200,Gramlib.Gramext.RightA,true;
+   100,Gramlib.Gramext.RightA,false;
+   99,Gramlib.Gramext.RightA,true;
+   90,Gramlib.Gramext.RightA,true;
+   10,Gramlib.Gramext.LeftA,false;
+   1,Gramlib.Gramext.LeftA,false;
+   0,Gramlib.Gramext.RightA,false]
 
 let default_constr_levels = (default_levels, default_pattern_levels)
 
@@ -70,28 +70,28 @@ let save_levels levels custom lev =
 (* first LeftA, then RightA and NoneA together *)
 
 let admissible_assoc = function
-  | Extend.LeftA, Some (Extend.RightA | Extend.NonA) -> false
-  | Extend.RightA, Some Extend.LeftA -> false
+  | Gramlib.Gramext.LeftA, Some (Gramlib.Gramext.RightA | Gramlib.Gramext.NonA) -> false
+  | Gramlib.Gramext.RightA, Some Gramlib.Gramext.LeftA -> false
   | _ -> true
 
 let create_assoc = function
-  | None -> Extend.RightA
+  | None -> Gramlib.Gramext.RightA
   | Some a -> a
 
 let error_level_assoc p current expected =
   let open Pp in
   let pr_assoc = function
-    | Extend.LeftA -> str "left"
-    | Extend.RightA -> str "right"
-    | Extend.NonA -> str "non" in
+    | Gramlib.Gramext.LeftA -> str "left"
+    | Gramlib.Gramext.RightA -> str "right"
+    | Gramlib.Gramext.NonA -> str "non" in
   user_err 
     (str "Level " ++ int p ++ str " is already declared " ++
      pr_assoc current ++ str " associative while it is now expected to be " ++
      pr_assoc expected ++ str " associative.")
 
 let create_pos = function
-  | None -> Extend.First
-  | Some lev -> Extend.After (constr_level lev)
+  | None -> Gramlib.Gramext.First
+  | Some lev -> Gramlib.Gramext.After (constr_level lev)
 
 let find_position_gen current ensure assoc lev =
   match lev with
@@ -121,13 +121,13 @@ let find_position_gen current ensure assoc lev =
 	   updated, (Some (create_pos !after), Some assoc, Some (constr_level n), None)
         | _ ->
 	  (* The reinit flag has been updated *)
-	   updated, (Some (Extend.Level (constr_level n)), None, None, !init)
+           updated, (Some (Gramlib.Gramext.Level (constr_level n)), None, None, !init)
         end
       with
 	  (* Nothing has changed *)
           Exit ->
 	    (* Just inherit the existing associativity and name (None) *)
-	    current, (Some (Extend.Level (constr_level n)), None, None, None)
+            current, (Some (Gramlib.Gramext.Level (constr_level n)), None, None, None)
 
 let rec list_mem_assoc_triple x = function
   | [] -> false
@@ -186,15 +186,18 @@ let find_position accu custom forpat assoc level =
 (* Binding constr entry keys to entries                               *)
 
 (* Camlp5 levels do not treat NonA: use RightA with a NEXT on the left *)
-let camlp5_assoc = function
-  | Some NonA | Some RightA -> RightA
-  | None | Some LeftA -> LeftA
-
-let assoc_eq al ar = match al, ar with
-| NonA, NonA
-| RightA, RightA
-| LeftA, LeftA -> true
-| _, _ -> false
+let camlp5_assoc =
+  let open Gramlib.Gramext in function
+    | Some NonA | Some RightA -> RightA
+    | None | Some LeftA -> LeftA
+
+let assoc_eq al ar =
+  let open Gramlib.Gramext in
+  match al, ar with
+  | NonA, NonA
+  | RightA, RightA
+  | LeftA, LeftA -> true
+  | _, _ -> false
 
 (* [adjust_level assoc from prod] where [assoc] and [from] are the name
    and associativity of the level where to add the rule; the meaning of
@@ -204,7 +207,7 @@ let assoc_eq al ar = match al, ar with
      Some None = NEXT
      Some (Some (n,cur)) = constr LEVEL n
          s.t. if [cur] is set then [n] is the same as the [from] level *)
-let adjust_level assoc from = function
+let adjust_level assoc from = let open Gramlib.Gramext in function
 (* Associativity is None means force the level *)
   | (NumLevel n,BorderProd (_,None)) -> Some (Some (n,true))
 (* Compute production name on the right side *)
diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg
index e3f6a87541..22528a607f 100644
--- a/vernac/g_vernac.mlg
+++ b/vernac/g_vernac.mlg
@@ -1175,9 +1175,9 @@ GRAMMAR EXTEND Gram
       | "in"; IDENT "custom"; x = IDENT -> { SetCustomEntry (x,None) }
       | "in"; IDENT "custom"; x = IDENT; "at"; IDENT "level"; n = natural ->
          { SetCustomEntry (x,Some n) }
-      | IDENT "left"; IDENT "associativity" -> { SetAssoc LeftA }
-      | IDENT "right"; IDENT "associativity" -> { SetAssoc RightA }
-      | IDENT "no"; IDENT "associativity" -> { SetAssoc NonA }
+      | IDENT "left"; IDENT "associativity" -> { SetAssoc Gramlib.Gramext.LeftA }
+      | IDENT "right"; IDENT "associativity" -> { SetAssoc Gramlib.Gramext.RightA }
+      | IDENT "no"; IDENT "associativity" -> { SetAssoc Gramlib.Gramext.NonA }
       | IDENT "only"; IDENT "printing" -> { SetOnlyPrinting }
       | IDENT "only"; IDENT "parsing" -> { SetOnlyParsing }
       | IDENT "compat"; s = STRING ->
diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml
index 5ab877fae2..82434afbbd 100644
--- a/vernac/metasyntax.ml
+++ b/vernac/metasyntax.ml
@@ -287,7 +287,7 @@ let pr_notation_entry = function
   | InConstrEntry -> str "constr"
   | InCustomEntry s -> str "custom " ++ str s
 
-let prec_assoc = function
+let prec_assoc = let open Gramlib.Gramext in function
   | RightA -> (L,E)
   | LeftA -> (E,L)
   | NonA -> (L,L)
@@ -685,7 +685,7 @@ let border = function
   | (_,(ETConstr(_,_,(_,BorderProd (_,a))))) :: _ -> a
   | _ -> None
 
-let recompute_assoc typs =
+let recompute_assoc typs = let open Gramlib.Gramext in
   match border typs, border (List.rev typs) with
     | Some LeftA, Some RightA -> assert false
     | Some LeftA, _ -> Some LeftA
@@ -802,7 +802,7 @@ let inSyntaxExtension : syntax_extension_obj -> obj =
 module NotationMods = struct
 
 type notation_modifier = {
-  assoc         : gram_assoc option;
+  assoc         : Gramlib.Gramext.g_assoc option;
   level         : int option;
   custom        : notation_entry;
   etyps         : (Id.t * simple_constr_prod_entry_key) list;
@@ -1230,7 +1230,7 @@ let compute_syntax_data local df modifiers =
   let onlyprint = mods.only_printing in
   let onlyparse = mods.only_parsing in
   if onlyprint && onlyparse then user_err (str "A notation cannot be both 'only printing' and 'only parsing'.");
-  let assoc = Option.append mods.assoc (Some NonA) in
+  let assoc = Option.append mods.assoc (Some Gramlib.Gramext.NonA) in
   let (recvars,mainvars,symbols) = analyze_notation_tokens ~onlyprint df in
   let _ = check_useless_entry_types recvars mainvars mods.etyps in
   let _ = check_binder_type recvars mods.etyps in
diff --git a/vernac/ppvernac.ml b/vernac/ppvernac.ml
index 2ddd210365..e7c1e29beb 100644
--- a/vernac/ppvernac.ml
+++ b/vernac/ppvernac.ml
@@ -380,7 +380,7 @@ open Pputils
 
   let pr_thm_token k = keyword (Kindops.string_of_theorem_kind k)
 
-  let pr_syntax_modifier = function
+  let pr_syntax_modifier = let open Gramlib.Gramext in function
     | SetItemLevel (l,bko,n) ->
       prlist_with_sep sep_v2 str l ++ spc () ++ pr_at_level_opt n ++
       pr_opt pr_constr_as_binder_kind bko
diff --git a/vernac/vernacexpr.ml b/vernac/vernacexpr.ml
index 122005e011..1e6c40c829 100644
--- a/vernac/vernacexpr.ml
+++ b/vernac/vernacexpr.ml
@@ -167,7 +167,7 @@ type syntax_modifier =
   | SetItemLevel of string list * Notation_term.constr_as_binder_kind option * Extend.production_level option
   | SetLevel of int
   | SetCustomEntry of string * int option
-  | SetAssoc of Extend.gram_assoc
+  | SetAssoc of Gramlib.Gramext.g_assoc
   | SetEntryType of string * Extend.simple_constr_prod_entry_key
   | SetOnlyParsing
   | SetOnlyPrinting