From 5a39e6c08d428d774165e0ef3922ba8b75eee9e1 Mon Sep 17 00:00:00 2001 From: ppedrot Date: Mon, 28 Jan 2013 21:05:35 +0000 Subject: Uniformization of the "anomaly" command. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16165 85f007b7-540e-0410-9357-904b9bb8a0f7 --- library/lib.ml | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) (limited to 'library/lib.ml') diff --git a/library/lib.ml b/library/lib.ml index 0f2f480cb..01e24f6c7 100644 --- a/library/lib.ml +++ b/library/lib.ml @@ -350,15 +350,15 @@ let end_compilation dir = try match find_entry_p is_opening_lib with | (oname, CompilingLibrary prefix) -> oname | _ -> assert false - with Not_found -> anomaly "No module declared" + with Not_found -> anomaly (Pp.str "No module declared") in let _ = match !comp_name with - | None -> anomaly "There should be a module name..." + | None -> anomaly (Pp.str "There should be a module name...") | Some m -> if not (Names.Dir_path.equal m dir) then anomaly - ("The current open module has name "^ (Names.Dir_path.to_string m) ^ - " and not " ^ (Names.Dir_path.to_string m)); + (str "The current open module has name" ++ spc () ++ pr_dirpath m ++ + spc () ++ str "and not" ++ spc () ++ pr_dirpath m); in let (after,mark,before) = split_lib_at_opening oname in comp_name := None; @@ -521,7 +521,7 @@ let discharge_item ((sp,_ as oname),e) = | FrozenState _ -> None | ClosedSection _ | ClosedModule _ -> None | OpenedSection _ | OpenedModule _ | CompilingLibrary _ -> - anomaly "discharge_item" + anomaly (Pp.str "discharge_item") let close_section () = let oname,fs = @@ -681,7 +681,7 @@ let remove_section_part ref = let dir,_ = repr_path sp in match ref with | VarRef id -> - anomaly "remove_section_part not supported on local variables" + anomaly (Pp.str "remove_section_part not supported on local variables") | _ -> if is_dirpath_prefix_of dir (cwd ()) then (* Not yet (fully) discharged *) -- cgit v1.2.3