From ade5ae3ee5931180211260b943e5095188518c03 Mon Sep 17 00:00:00 2001 From: notin Date: Tue, 12 Sep 2006 14:52:07 +0000 Subject: Indentation + svnprop git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9133 85f007b7-540e-0410-9357-904b9bb8a0f7 --- library/lib.ml | 11 ++++++----- library/library.ml | 2 +- 2 files changed, 7 insertions(+), 6 deletions(-) (limited to 'library') diff --git a/library/lib.ml b/library/lib.ml index 40590a220..49e685f63 100644 --- a/library/lib.ml +++ b/library/lib.ml @@ -319,7 +319,7 @@ let end_compilation dir = | _, OpenedModtype _ -> error "There are some open module types" | _ -> assert false with - Not_found -> () + Not_found -> () in let module_p = function (_,CompilingLibrary _) -> true | x -> is_something_opened x @@ -331,16 +331,17 @@ let end_compilation dir = with Not_found -> anomaly "No module declared" in - let _ = match !comp_name with + let _ = + match !comp_name with | None -> anomaly "There should be a module name..." | Some m -> if m <> dir then anomaly ("The current open module has name "^ (string_of_dirpath m) ^ - " and not " ^ (string_of_dirpath m)); + " and not " ^ (string_of_dirpath m)); in let (after,_,before) = split_lib oname in - comp_name := None; - !path_prefix,after + comp_name := None; + !path_prefix,after (* Returns true if we are inside an opened module type *) let is_modtype () = diff --git a/library/library.ml b/library/library.ml index 73d58b549..2412f67a1 100644 --- a/library/library.ml +++ b/library/library.ml @@ -606,7 +606,7 @@ let save_library_to dir f = let di = Digest.file f' in System.marshal_out ch di; close_out ch - with e -> (warning ("Removed file "^f');close_out ch; Sys.remove f'; raise e) + with e -> (warning ("Removed file "^f'); close_out ch; Sys.remove f'; raise e) (************************************************************************) (*s Display the memory use of a library. *) -- cgit v1.2.3