From 928e1c69588a2057c8d30a2bb4c3fe140cfe025f Mon Sep 17 00:00:00 2001
From: herbelin
Date: Wed, 7 Jan 2009 20:48:01 +0000
Subject: Uniformisation of some error messages + added test on setoid rewrite.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11765 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 library/lib.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'library')

diff --git a/library/lib.ml b/library/lib.ml
index 7135a93cc0..dfe00fae51 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -575,11 +575,11 @@ let close_section id =
       | oname,OpenedSection (_,fs) -> 
 	  let id' = basename (fst oname) in 
 	    if id <> id' then 
-	      errorlabstrm "close_section" (str "last opened section is " ++ pr_id id');
+	      errorlabstrm "close_section" (str "Last opened section is " ++ pr_id id' ++ str ".");
 	    (oname,fs)
       | _ -> assert false 
     with Not_found ->
-      error "no opened section"
+      error "No opened section."
   in
   let (secdecls,secopening,before) = split_lib oname in
   lib_stk := before;
-- 
cgit v1.2.3