diff options
| author |  notin <notin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2006-09-12 14:52:07 +0000 |
|---|---|---|
| committer | notin <notin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2006-09-12 14:52:07 +0000 |
| commit | ade5ae3ee5931180211260b943e5095188518c03 (patch) | |
| tree | 3303546664bf62dcbe65fba0d3083d25497ca46b /library/lib.ml | |
| parent | 87722d2a5d9592f08fafa2b4d56c9ba7aadd1033 (diff) | |
Indentation + svnprop
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9133 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'library/lib.ml')
| -rw-r--r-- | library/lib.ml | 11 |
1 files changed, 6 insertions, 5 deletions
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 () = |