From 7ba5db11d6e9704d3acb89ca1dbb7cd9890a4385 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Tue, 12 Aug 2003 12:58:58 +0000
Subject: Bug et améliorations diverses

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4264 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 interp/constrextern.ml | 7 ++++++-
 1 file changed, 6 insertions(+), 1 deletion(-)

(limited to 'interp')

diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 29f3c437c5..97e9855de8 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -125,8 +125,13 @@ let translate_keyword = function
     | "if"  | "then" | "else" | "return" as s) ->
       let s' = s^"_" in
       msgerrnl
-      (str ("Warning: "^s^" is now a keyword; it has been translated to "^s'));
+      (str ("Warning: '"^
+          s^"' is now a keyword; it has been translated to '"^s'^"'"));
       s'
+  | "_" -> 
+      msgerrnl (str 
+	"Warning: '_' is no longer a keyword; it has been translated to 'xx'");
+      "xx"
   | s -> s
 
 let is_coq_root d =
-- 
cgit v1.2.3