[gramlib] Remove warning function parameter in favor of standard mechanism.

If we need more fine-tuning we should manage the warnings with the
standard Coq mechanism.

6 files changed, 51 insertions, 63 deletions

diff --git a/coqpp/coqpp_main.ml b/coqpp/coqpp_main.ml
index 17f81c555c..0e0aefaaef 100644
--- a/coqpp/coqpp_main.ml
+++ b/coqpp/coqpp_main.ml
@@ -253,7 +253,7 @@ and print_symbol fmt tkn = match tkn with
     fprintf fmt "Pcoq.G.Rules.make @[(%a)@ (%a)@]" (print_symbols ~norec:true) tkn print_fun (vars, body)
   in
   let pr fmt rules = print_list fmt pr rules in
-  fprintf fmt "(Pcoq.G.Symbol.rules ~warning:None %a)" pr (List.rev rules)
+  fprintf fmt "(Pcoq.G.Symbol.rules %a)" pr (List.rev rules)
 | SymbQuote c ->
   fprintf fmt "(%s)" c
 
diff --git a/gramlib/grammar.ml b/gramlib/grammar.ml
index ac6f752670..814844508b 100644
--- a/gramlib/grammar.ml
+++ b/gramlib/grammar.ml
@@ -63,7 +63,7 @@ module type S = sig
     val self : ('self, mayrec, 'self) t
     val next : ('self, mayrec, 'self) t
     val token : 'c pattern -> ('self, norec, 'c) t
-    val rules : warning:(string -> unit) option -> 'a Rules.t list -> ('self, norec, 'a) t
+    val rules : 'a Rules.t list -> ('self, norec, 'a) t
 
   end and Rule : sig
 
@@ -101,7 +101,7 @@ module type S = sig
     ; data : 'a single_extend_statement list
     }
 
-  val safe_extend : warning:(string -> unit) option -> 'a Entry.t -> 'a extend_statement -> unit
+  val safe_extend : 'a Entry.t -> 'a extend_statement -> unit
   val safe_delete_rule : 'a Entry.t -> 'a Production.t -> unit
 
   val generalize_symbol : ('a, 'tr, 'c) Symbol.t -> ('a, norec, 'c) Symbol.t option
@@ -348,7 +348,7 @@ let and_and_tree (type s tr' trt tr trn trs trb f) (ar : (tr', trt, tr) ty_and_r
   | MayRec2, _, MayRec -> MayRec2 | MayRec2, _, NoRec -> MayRec2
   | NoRec2, NoRec3, NoRec -> NoRec2
 
-let insert_tree (type s trs trt tr p k a) ~warning entry_name (ar : (trs, trt, tr) ty_and_ex) (gsymbols : (s, trs, p) ty_symbols) (pf : (p, k, a) rel_prod) (action : k) (tree : (s, trt, a) ty_tree) : (s, tr, a) ty_tree =
+let insert_tree (type s trs trt tr p k a) entry_name (ar : (trs, trt, tr) ty_and_ex) (gsymbols : (s, trs, p) ty_symbols) (pf : (p, k, a) rel_prod) (action : k) (tree : (s, trt, a) ty_tree) : (s, tr, a) ty_tree =
   let rec insert : type trs trt tr p f k. (trs, trt, tr) ty_and_ex -> (s, trs, p) ty_symbols -> (p, k, f) rel_prod -> (s, trt, f) ty_tree -> k -> (s, tr, f) ty_tree  =
     fun ar symbols pf tree action ->
     match symbols, pf with
@@ -362,15 +362,15 @@ let insert_tree (type s trs trt tr p k a) ~warning entry_name (ar : (trs, trt, t
         | NR10, Node (_, n) -> Node (MayRec3, node n)
         | NR11, Node (NoRec3, n) -> Node (NoRec3, node n)
         | NR11, LocAct (old_action, action_list) ->
-          begin match warning with
-            | None -> ()
-            | Some warn_fn ->
+          (* What to do about this warning? For now it is disabled *)
+          if false then
+            begin
               let msg =
                 "<W> Grammar extension: " ^
                 (if entry_name = "" then "" else "in ["^entry_name^"%s], ") ^
                 "some rule has been masked" in
-              warn_fn msg
-          end;
+              Feedback.msg_warning (Pp.str msg)
+            end;
           LocAct (action, old_action :: action_list)
         | NR11, DeadEnd -> LocAct (action, [])
   and insert_in_tree : type trs trs' trs'' trt tr a p f k. (trs'', trt, tr) ty_and_ex -> (trs, trs', trs'') ty_and_rec -> (s, trs, a) ty_symbol -> (s, trs', p) ty_symbols -> (p, k, a -> f) rel_prod -> (s, trt, f) ty_tree -> k -> (s, tr, f) ty_tree =
@@ -429,14 +429,14 @@ let insert_tree (type s trs trt tr p k a) ~warning entry_name (ar : (trs, trt, t
   in
   insert ar gsymbols pf tree action
 
-let insert_tree_norec (type s p k a) ~warning entry_name (gsymbols : (s, norec, p) ty_symbols) (pf : (p, k, a) rel_prod) (action : k) (tree : (s, norec, a) ty_tree) : (s, norec, a) ty_tree =
-  insert_tree ~warning entry_name NR11 gsymbols pf action tree
+let insert_tree_norec (type s p k a) entry_name (gsymbols : (s, norec, p) ty_symbols) (pf : (p, k, a) rel_prod) (action : k) (tree : (s, norec, a) ty_tree) : (s, norec, a) ty_tree =
+  insert_tree entry_name NR11 gsymbols pf action tree
 
-let insert_tree (type s trs trt p k a) ~warning entry_name (gsymbols : (s, trs, p) ty_symbols) (pf : (p, k, a) rel_prod) (action : k) (tree : (s, trt, a) ty_tree) : (s, a) ty_mayrec_tree =
+let insert_tree (type s trs trt p k a) entry_name (gsymbols : (s, trs, p) ty_symbols) (pf : (p, k, a) rel_prod) (action : k) (tree : (s, trt, a) ty_tree) : (s, a) ty_mayrec_tree =
   let MayRecNR ar = and_symbols_tree gsymbols tree in
-  MayRecTree (insert_tree ~warning entry_name ar gsymbols pf action tree)
+  MayRecTree (insert_tree entry_name ar gsymbols pf action tree)
 
-let srules (type self a) ~warning (rl : a ty_rules list) : (self, norec, a) ty_symbol =
+let srules (type self a) (rl : a ty_rules list) : (self, norec, a) ty_symbol =
   let rec retype_tree : type s a. (s, norec, a) ty_tree -> (self, norec, a) ty_tree =
     function
     | Node (NoRec3, {node = s; son = son; brother = bro}) ->
@@ -463,7 +463,7 @@ let srules (type self a) ~warning (rl : a ty_rules list) : (self, norec, a) ty_s
       (fun tree (TRules (symbols, action)) ->
         let symbols = retype_rule symbols in
         let AnyS (symbols, pf) = get_symbols symbols in
-        insert_tree_norec ~warning "" symbols pf action tree)
+        insert_tree_norec "" symbols pf action tree)
       DeadEnd rl
   in
   Stree t
@@ -473,19 +473,19 @@ let is_level_labelled n (Level lev) =
     Some n1 -> n = n1
   | None -> false
 
-let insert_level (type s tr p k) ~warning entry_name (symbols : (s, tr, p) ty_symbols) (pf : (p, k, Loc.t -> s) rel_prod) (action : k) (slev : s ty_level) : s ty_level =
+let insert_level (type s tr p k) entry_name (symbols : (s, tr, p) ty_symbols) (pf : (p, k, Loc.t -> s) rel_prod) (action : k) (slev : s ty_level) : s ty_level =
   match symbols with
   | TCns (_, Sself, symbols) ->
       let Level slev = slev in
       let RelS pf = pf in
-      let MayRecTree lsuffix = insert_tree ~warning entry_name symbols pf action slev.lsuffix in
+      let MayRecTree lsuffix = insert_tree entry_name symbols pf action slev.lsuffix in
       Level
       {assoc = slev.assoc; lname = slev.lname;
        lsuffix = lsuffix;
        lprefix = slev.lprefix}
   | _ ->
       let Level slev = slev in
-      let MayRecTree lprefix = insert_tree ~warning entry_name symbols pf action slev.lprefix in
+      let MayRecTree lprefix = insert_tree entry_name symbols pf action slev.lprefix in
       Level
       {assoc = slev.assoc; lname = slev.lname; lsuffix = slev.lsuffix;
        lprefix = lprefix}
@@ -499,34 +499,27 @@ let empty_lev lname assoc =
   Level
   {assoc = assoc; lname = lname; lsuffix = DeadEnd; lprefix = DeadEnd}
 
-let change_lev ~warning (Level lev) n lname assoc =
+let change_lev (Level lev) n lname assoc =
   let a =
     match assoc with
       None -> lev.assoc
     | Some a ->
       if a <> lev.assoc then
-        begin
-          match warning with
-          | None -> ()
-          | Some warn_fn ->
-            warn_fn ("<W> Changing associativity of level \""^n^"\"")
-        end;
-        a
+        Feedback.msg_warning (Pp.str ("<W> Changing associativity of level \""^n^"\""));
+      a
   in
-  begin match lname with
-    Some n ->
-      if lname <> lev.lname then
-        begin match warning with
-          | None -> ()
-          | Some warn_fn ->
-            warn_fn ("<W> Level label \""^n^"\" ignored")
-        end;
-  | None -> ()
+  begin
+    match lname with
+    | Some n ->
+      (* warning disabled; it was in the past *)
+      if false && lname <> lev.lname then
+        Feedback.msg_warning (Pp.str ("<W> Level label \""^n^"\" ignored"))
+    | None -> ()
   end;
   Level
   {assoc = a; lname = lev.lname; lsuffix = lev.lsuffix; lprefix = lev.lprefix}
 
-let get_level ~warning entry position levs =
+let get_level entry position levs =
   match position with
     Some First -> [], empty_lev, levs
   | Some Last -> levs, empty_lev, []
@@ -539,7 +532,7 @@ let get_level ~warning entry position levs =
             flush stderr;
             failwith "Grammar.extend"
         | lev :: levs ->
-            if is_level_labelled n lev then [], change_lev ~warning lev n, levs
+            if is_level_labelled n lev then [], change_lev lev n, levs
             else
               let (levs1, rlev, levs2) = get levs in lev :: levs1, rlev, levs2
       in
@@ -574,7 +567,7 @@ let get_level ~warning entry position levs =
       get levs
   | None ->
       match levs with
-        lev :: levs -> [], change_lev ~warning lev "<top>", levs
+        lev :: levs -> [], change_lev lev "<top>", levs
       | [] -> [], empty_lev, []
 
 let change_to_self0 (type s) (type trec) (type a) (entry : s ty_entry) : (s, trec, a) ty_symbol -> (s, a) ty_mayrec_symbol =
@@ -624,7 +617,7 @@ let insert_tokens gram symbols =
   in
   linsert symbols
 
-let levels_of_rules ~warning entry position rules =
+let levels_of_rules entry position rules =
   let elev =
     match entry.edesc with
       Dlevels elev -> elev
@@ -636,7 +629,7 @@ let levels_of_rules ~warning entry position rules =
   match rules with
   | [] -> elev
   | _ ->
-    let (levs1, make_lev, levs2) = get_level ~warning entry position elev in
+    let (levs1, make_lev, levs2) = get_level entry position elev in
     let (levs, _) =
       List.fold_left
         (fun (levs, make_lev) (lname, assoc, level) ->
@@ -647,7 +640,7 @@ let levels_of_rules ~warning entry position rules =
                   let MayRecRule symbols = change_to_self entry symbols in
                   let AnyS (symbols, pf) = get_symbols symbols in
                   insert_tokens egram symbols;
-                  insert_level ~warning entry.ename symbols pf action lev)
+                  insert_level entry.ename symbols pf action lev)
                lev level
            in
            lev :: levs, empty_lev)
@@ -1503,8 +1496,8 @@ let init_entry_functions entry =
        let f = continue_parser_of_entry entry in
        entry.econtinue <- f; f lev bp a strm)
 
-let extend_entry ~warning entry position rules =
-    let elev = levels_of_rules ~warning entry position rules in
+let extend_entry entry position rules =
+    let elev = levels_of_rules entry position rules in
     entry.edesc <- Dlevels elev; init_entry_functions entry
 
 (* Deleting a rule *)
@@ -1630,7 +1623,7 @@ module rec Symbol : sig
   val self : ('self, mayrec, 'self) t
   val next : ('self, mayrec, 'self) t
   val token : 'c pattern -> ('self, norec, 'c) t
-  val rules : warning:(string -> unit) option -> 'a Rules.t list -> ('self, norec, 'a) t
+  val rules : 'a Rules.t list -> ('self, norec, 'a) t
 
 end = struct
 
@@ -1645,7 +1638,7 @@ end = struct
   let self = Sself
   let next = Snext
   let token tok = Stoken tok
-  let rules ~warning (t : 'a Rules.t list) = srules ~warning t
+  let rules (t : 'a Rules.t list) = srules t
 
 end and Rule : sig
 
@@ -1705,8 +1698,8 @@ type 'a extend_statement =
   ; data : 'a single_extend_statement list
   }
 
-let safe_extend ~warning (e : 'a Entry.t) { pos; data } =
-  extend_entry ~warning e pos data
+let safe_extend (e : 'a Entry.t) { pos; data } =
+  extend_entry e pos data
 
 let safe_delete_rule e (TProd (r,_act)) =
   let AnyS (symbols, _) = get_symbols r in
diff --git a/gramlib/grammar.mli b/gramlib/grammar.mli
index 7738e32cab..16e147de3b 100644
--- a/gramlib/grammar.mli
+++ b/gramlib/grammar.mli
@@ -30,7 +30,6 @@ module type GLexerType = sig
   end
 end
 
-
 type norec
 type mayrec
 
@@ -73,7 +72,7 @@ module type S = sig
     val self : ('self, mayrec, 'self) t
     val next : ('self, mayrec, 'self) t
     val token : 'c pattern -> ('self, norec, 'c) t
-    val rules : warning:(string -> unit) option -> 'a Rules.t list -> ('self, norec, 'a) t
+    val rules : 'a Rules.t list -> ('self, norec, 'a) t
 
   end and Rule : sig
 
@@ -111,7 +110,7 @@ module type S = sig
     ; data : 'a single_extend_statement list
     }
 
-  val safe_extend : warning:(string -> unit) option -> 'a Entry.t -> 'a extend_statement -> unit
+  val safe_extend : 'a Entry.t -> 'a extend_statement -> unit
   val safe_delete_rule : 'a Entry.t -> 'a Production.t -> unit
 
   val generalize_symbol : ('a, 'tr, 'c) Symbol.t -> ('a, norec, 'c) Symbol.t option
diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml
index 59f92e7790..fe280c1f69 100644
--- a/parsing/pcoq.ml
+++ b/parsing/pcoq.ml
@@ -127,25 +127,24 @@ let grammar_delete_reinit e reinit ({ G.pos; data } as d)=
     | Some (Gramext.Level n) -> n
     | _ -> assert false
   in
-  let warning msg = Feedback.msg_warning Pp.(str msg) in
   let ext = { G.pos = Some ext; data = [Some lev,Some a,[]] } in
-  G.safe_extend ~warning:(Some warning) e ext
+  G.safe_extend e ext
 
 (** Extension *)
 
 let grammar_extend e ext =
   let undo () = grammar_delete e ext in
-  let redo () = G.safe_extend ~warning:None e ext in
+  let redo () = G.safe_extend e ext in
   camlp5_state := ByEXTEND (undo, redo) :: !camlp5_state;
   redo ()
 
 let grammar_extend_sync e ext =
   camlp5_state := ByGrammar (ExtendRule (e, ext)) :: !camlp5_state;
-  G.safe_extend ~warning:None e ext
+  G.safe_extend e ext
 
 let grammar_extend_sync_reinit e reinit ext =
   camlp5_state := ByGrammar (ExtendRuleReinit (e, reinit, ext)) :: !camlp5_state;
-  G.safe_extend ~warning:None e ext
+  G.safe_extend e ext
 
 (** Remove extensions
 
@@ -189,18 +188,16 @@ let eoi_entry en =
   let e = G.Entry.make ((G.Entry.name en) ^ "_eoi") in
   let symbs = G.Rule.next (G.Rule.next G.Rule.stop (G.Symbol.nterm en)) (G.Symbol.token Tok.PEOI) in
   let act = fun _ x loc -> x in
-  let warning msg = Feedback.msg_warning Pp.(str msg) in
   let ext = { G.pos = None; data = make_rule [G.Production.make symbs act] } in
-  G.safe_extend ~warning:(Some warning) e ext;
+  G.safe_extend e ext;
   e
 
 let map_entry f en =
   let e = G.Entry.make ((G.Entry.name en) ^ "_map") in
   let symbs = G.Rule.next G.Rule.stop (G.Symbol.nterm en) in
   let act = fun x loc -> f x in
-  let warning msg = Feedback.msg_warning Pp.(str msg) in
   let ext = { G.pos = None; data = make_rule [G.Production.make symbs act] } in
-  G.safe_extend ~warning:(Some warning) e ext;
+  G.safe_extend e ext;
   e
 
 (* Parse a string, does NOT check if the entire string was read
@@ -348,9 +345,8 @@ module Module =
 let epsilon_value (type s tr a) f (e : (s, tr, a) G.Symbol.t) =
   let r = G.Production.make (G.Rule.next G.Rule.stop e) (fun x _ -> f x) in
   let entry = G.Entry.make "epsilon" in
-  let warning msg = Feedback.msg_warning Pp.(str msg) in
   let ext = { G.pos = None; data = [None, None, [r]] } in
-  let () = G.safe_extend ~warning:(Some warning) entry ext in
+  let () = G.safe_extend entry ext in
   try Some (parse_string entry "") with _ -> None
 
 (** Synchronized grammar extensions *)
diff --git a/user-contrib/Ltac2/tac2core.ml b/user-contrib/Ltac2/tac2core.ml
index 920be6db5b..ab660b486e 100644
--- a/user-contrib/Ltac2/tac2core.ml
+++ b/user-contrib/Ltac2/tac2core.ml
@@ -1614,7 +1614,7 @@ let rec make_seq_rule = function
 let () = add_scope "seq" begin fun toks ->
   let scope =
     let Seqrule (r, c) = make_seq_rule (List.rev toks) in
-    Pcoq.G.(Symbol.rules ~warning:None [Rules.make r (apply c [])])
+    Pcoq.G.(Symbol.rules [Rules.make r (apply c [])])
   in
   Tac2entries.ScopeRule (scope, (fun e -> e))
 end
diff --git a/vernac/egramcoq.ml b/vernac/egramcoq.ml
index 7a52f53dc0..c4f15a40ce 100644
--- a/vernac/egramcoq.ml
+++ b/vernac/egramcoq.ml
@@ -329,7 +329,7 @@ let make_sep_rules = function
     Pcoq.G.Symbol.token tk
   | tkl ->
     let r = Pcoq.G.mk_rule (List.rev tkl) in
-    Pcoq.G.Symbol.rules ~warning:None [r]
+    Pcoq.G.Symbol.rules [r]
 
 type ('s, 'a) mayrec_symbol =
 | MayRecNo : ('s, Gramlib.Grammar.norec, 'a) G.Symbol.t -> ('s, 'a) mayrec_symbol