From f0226504cfb179a4491d43764bfdb22a1fe2d106 Mon Sep 17 00:00:00 2001 From: herbelin Date: Sat, 17 Dec 2011 20:53:35 +0000 Subject: A pass on warning printings. Made systematic the use of msg_warning so as to ensure the warning is flushed in real time. Made systematic the use of if_warn instead of if_verbose when the warning is intended to signal something anormal (if_warn is activated when compiling verbosely and when working interactively while if_verbose is activated only when working interactively and when loading verbosely). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14803 85f007b7-540e-0410-9357-904b9bb8a0f7 --- pretyping/pattern.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'pretyping/pattern.ml') diff --git a/pretyping/pattern.ml b/pretyping/pattern.ml index 585de58fb..65f342d88 100644 --- a/pretyping/pattern.ml +++ b/pretyping/pattern.ml @@ -300,8 +300,8 @@ let rec pat_of_raw metas vars = function | GHole _ -> PMeta None | GCast (_,c,_) -> - Flags.if_verbose - Pp.warning "Cast not taken into account in constr pattern"; + Flags.if_warn + Pp.msg_warning (str "Cast not taken into account in constr pattern"); pat_of_raw metas vars c | GIf (_,c,(_,None),b1,b2) -> PIf (pat_of_raw metas vars c, -- cgit v1.2.3