diff --git a/src/main.ml b/src/main.ml
index de083bb5bac4bcdceffcdb9d11589f80312397b2..7cd49bb7c4effb4054a833de72565ba73bb8ee7b 100644
--- a/src/main.ml
+++ b/src/main.ml
@@ -102,6 +102,9 @@ let opt_command = ref None
 let opt_task = ref None
 let opt_bisect = ref false
 
+let opt_print_libdir = ref false
+let opt_print_datadir = ref false
+
 let opt_print_theory = ref false
 let opt_print_namespace = ref false
 let opt_list_transforms = ref false
@@ -199,17 +202,28 @@ let option_list = Arg.align [
       " Set all debug flags (except parse_only and type_only)";
   "--debug", Arg.String add_opt_debug,
       "<flag> Set a debug flag";
+  "--print-libdir", Arg.Set opt_print_libdir,
+      " Print location of binary components (plugins, etc)";
+  "--print-datadir", Arg.Set opt_print_datadir,
+      " Print location of non-binary data (theories, modules, etc)";
   "--version", Arg.Set opt_version,
       " Print version information" ]
 
-let () =
-  try
+let () = try
   Arg.parse option_list add_opt_file usage_msg;
 
   if !opt_version then begin
     printf "%s@." version_msg;
     exit 0
   end;
+  if !opt_print_libdir then begin
+    printf "%s@." Config.libdir;
+    exit 0
+  end;
+  if !opt_print_datadir then begin
+    printf "%s@." Config.datadir;
+    exit 0
+  end;
 
   (** Debug flag *)
   if !opt_debug_all then begin
@@ -322,7 +336,6 @@ let () =
     exit 1
   end;
 
-
   opt_loadpath := List.rev_append !opt_loadpath (Whyconf.loadpath main);
   if !opt_timelimit = None then opt_timelimit := Some (Whyconf.timelimit main);
   if !opt_memlimit  = None then opt_memlimit  := Some (Whyconf.memlimit main);
@@ -341,6 +354,7 @@ let () =
     add_meta task meta [MAstr s]
   in
   opt_task := List.fold_left add_meta !opt_task !opt_metas
+
   with e when not (Debug.test_flag Debug.stack_trace) ->
     eprintf "%a@." Exn_printer.exn_printer e;
     exit 1
@@ -500,7 +514,7 @@ let do_input env drv = function
       close_in cin;
       if !opt_type_only then
         ()
-      else 
+      else
 	match !opt_coq_realization with
 	  | Some f ->
 	      Queue.iter (do_coq_realize_theory env drv f fname m) tlist
diff --git a/src/util/loc.ml b/src/util/loc.ml
index 7909caee4048a12d7ac883ff62867de61a27d313..92ecf2270df1097b72baec30e6a66fbf6858510d 100644
--- a/src/util/loc.ml
+++ b/src/util/loc.ml
@@ -76,22 +76,13 @@ let compare (_,l1,b1,e1) (_,l2,b2,e2) =
   Pervasives.compare e1 e2
 
 let gen_report_position fmt (f,l,b,e) =
-  fprintf fmt "File \"%s\", " f;
-  fprintf fmt "line %d, characters %d-%d" l b e
-
-let string =
-  let buf = Buffer.create 1024 in
-  fun loc ->
-    let fmt = Format.formatter_of_buffer buf in
-    Format.fprintf fmt "%a@?" gen_report_position loc;
-    let s = Buffer.contents buf in
-    Buffer.reset buf;
-    s
+  fprintf fmt "File \"%s\", line %d, characters %d-%d" f l b e
+
+let report_position fmt = fprintf fmt "%a:@\n" gen_report_position
 
 let () = Exn_printer.register
   (fun fmt exn -> match exn with
     | Located (loc,e) ->
-      fprintf fmt "%a:@\n%a@\n" gen_report_position loc
-        Exn_printer.exn_printer e
+        fprintf fmt "%a%a" report_position loc Exn_printer.exn_printer e
     | _ -> raise exn)
 
diff --git a/src/util/loc.mli b/src/util/loc.mli
index 57d5a883f6906943b509836ccccfe41f736d95c5..b13c01e445d1c3885acffe9d8139ab5e8ff42c54 100644
--- a/src/util/loc.mli
+++ b/src/util/loc.mli
@@ -36,8 +36,6 @@ val join : position -> position -> position
 
 exception Located of position * exn
 
-val string : position -> string
-
 val dummy_position : position
 
 val user_position : string -> int -> int -> int -> position
@@ -48,4 +46,5 @@ val compare : position -> position -> int
 
 val gen_report_position : formatter -> position -> unit
 
+val report_position : formatter -> position -> unit