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.
---
 coqpp/coqpp_main.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'coqpp')

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