diff options
Diffstat (limited to 'library')
| -rw-r--r-- | library/lib.ml | 4 |
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; |