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

1 files changed, 2 insertions, 2 deletions

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;