From 9dd2df4c16078d41df1cf6233c9cf84fffbeee52 Mon Sep 17 00:00:00 2001
From: corbinea
Date: Wed, 31 Jan 2007 13:37:42 +0000
Subject: redirection of errors in coqide + dynamic warning printer (needed for
 tm_egg)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9566 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 parsing/tacextend.ml4    | 2 +-
 parsing/vernacextend.ml4 | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

(limited to 'parsing')

diff --git a/parsing/tacextend.ml4 b/parsing/tacextend.ml4
index 442bbb6aff..7e32879d2a 100644
--- a/parsing/tacextend.ml4
+++ b/parsing/tacextend.ml4
@@ -64,7 +64,7 @@ let rec extract_signature = function
 let check_unicity s l =
   let l' = List.map (fun (l,_) -> extract_signature l) l in
   if not (Util.list_distinct l') then
-    Pp.warning_with Pp_control.err_ft
+    Pp.warning_with !Pp_control.err_ft
       ("Two distinct rules of tactic entry "^s^" have the same\n"^
       "non-terminals in the same order: put them in distinct tactic entries")
 
diff --git a/parsing/vernacextend.ml4 b/parsing/vernacextend.ml4
index 22df73ba73..5e8337fe97 100644
--- a/parsing/vernacextend.ml4
+++ b/parsing/vernacextend.ml4
@@ -56,7 +56,7 @@ let rec extract_signature = function
 let check_unicity s l =
   let l' = List.map (fun (_,l,_) -> extract_signature l) l in
   if not (Util.list_distinct l') then
-    Pp.warning_with Pp_control.err_ft
+    Pp.warning_with !Pp_control.err_ft
       ("Two distinct rules of entry "^s^" have the same\n"^
       "non-terminals in the same order: put them in distinct vernac entries")
 
-- 
cgit v1.2.3