diff options
| author | herbelin | 2011-11-30 10:55:17 +0000 |
|---|---|---|
| committer | herbelin | 2011-11-30 10:55:17 +0000 |
| commit | f045db6a3a8efc08d6db7fc58e5a59d786099555 (patch) | |
| tree | 9b4df60e7d458cd1f71bb6b9cdb05206f1aa7d2c | |
| parent | 6bee8342c0a914376688fba3927352f826aa9942 (diff) | |
Continuing r14747 being actually incomplete (flushing warnings and
printing them only if verbose).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14750 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | parsing/g_vernac.ml4 | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index 5cd67a8b0e..2dc72f658f 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -627,14 +627,16 @@ GEXTEND Gram (* moved there so that camlp5 factors it with the previous rule *) | IDENT "Arguments"; IDENT "Scope"; qid = smart_global; "["; scl = LIST0 [ "_" -> None | sc = IDENT -> Some sc ]; "]" -> - warning "Arguments Scope is deprecated; use Arguments instead"; + Flags.if_verbose + msg_warning (str "Arguments Scope is deprecated; use Arguments instead"); VernacArgumentsScope (use_section_locality (),qid,scl) (* Implicit *) | IDENT "Implicit"; IDENT "Arguments"; qid = smart_global; pos = LIST0 [ "["; l = LIST0 implicit_name; "]" -> List.map (fun (id,b,f) -> (ExplByName id,b,f)) l ] -> - warning "Implicit Arguments is deprecated; use Arguments instead"; + Flags.if_verbose + msg_warning (str "Implicit Arguments is deprecated; use Arguments instead"); VernacDeclareImplicits (use_section_locality (),qid,pos) | IDENT "Implicit"; "Type"; bl = reserv_list -> |