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.
---
 user-contrib/Ltac2/tac2core.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'user-contrib')

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