From 9847448b5f9dbf32806decf676f415d584a2cddb Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Fri, 21 Feb 2020 12:59:51 -0500
Subject: [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.
---
 vernac/egramcoq.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'vernac')

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
-- 
cgit v1.2.3