From 21c1f0f84540b8871e4c43fde114a7aedf165f60 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Wed, 12 May 2010 20:50:33 +0000
Subject: Missing warning flush in a lexer message + update of CHANGES

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

diff --git a/CHANGES b/CHANGES
index eb906205e9..6e1e218f59 100644
--- a/CHANGES
+++ b/CHANGES
@@ -1,3 +1,8 @@
+Changes from V8.3 to V8.4
+=========================
+
+New proof engine
+
 Changes from V8.2 to V8.3
 =========================
 
@@ -168,7 +173,7 @@ Vernacular commands
 
 Library
 
-- Use "Coq standard" names for the properties of eq and identity
+- Use "standard" Coq names for the properties of eq and identity
   (e.g. refl_equal is now eq_refl). Support for compatibility is provided.
 - The function Compare_dec.nat_compare is now defined directly,
   instead of relying on lt_eq_lt_dec. The earlier version is still
diff --git a/parsing/lexer.ml4 b/parsing/lexer.ml4
index afb26ec81e..9ca6533438 100644
--- a/parsing/lexer.ml4
+++ b/parsing/lexer.ml4
@@ -254,7 +254,7 @@ let rec string in_comments bp len = parser
       (parser
         | [< '')'; s >] ->
 	    if in_comments then
-	      warning "Not interpreting \"*)\" as the end of current non-terminated comment because it occurs in a non-terminated string of the comment.";
+	      msg_warning (str "Not interpreting \"*)\" as the end of current non-terminated comment because it occurs in a non-terminated string of the comment.");
 	    string in_comments bp (store (store len '*') ')') s
         | [< >] ->
 	    string in_comments bp (store len '*') s) s
-- 
cgit v1.2.3