From 001a56de3c85c1134e5901f23f6a4b8bb826518c Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sun, 15 Apr 2012 22:06:04 +0000
Subject: Adding newline after warning and restoring distinction between fatal
 and non fatal identifier check errors.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15178 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 kernel/names.ml | 8 ++++++--
 1 file changed, 6 insertions(+), 2 deletions(-)

(limited to 'kernel')

diff --git a/kernel/names.ml b/kernel/names.ml
index 735ab2899d..de1d7cce86 100644
--- a/kernel/names.ml
+++ b/kernel/names.ml
@@ -26,8 +26,12 @@ open Util
 
 type identifier = string
 
-let check_ident_soft x = Option.iter Pp.warning (ident_refutation x)
-let check_ident x = Option.iter Errors.error (ident_refutation x)
+let check_ident_soft x =
+  Option.iter (fun (fatal,x) ->
+      if fatal then error x else Pp.msg_warning (str x))
+    (ident_refutation x)
+let check_ident x =
+  Option.iter (fun (_,x) -> Errors.error x) (ident_refutation x)
 
 let id_of_string s = check_ident_soft s; String.copy s
 let string_of_id id = String.copy id
-- 
cgit v1.2.3