Merge branch 'v8.5' into trunk

Conflicts:
	tools/coq_makefile.ml

4 files changed, 16 insertions, 10 deletions

diff --git a/configure.ml b/configure.ml
index 4e2e34641a..d68fc505d0 100644
--- a/configure.ml
+++ b/configure.ml
@@ -11,11 +11,11 @@
 #load "str.cma"
 open Printf
 
-let coq_version = "trunk"
-let coq_macos_version = "8.4.90" (** "[...] should be a string comprised of
+let coq_version = "8.5beta1"
+let coq_macos_version = "8.5.91" (** "[...] should be a string comprised of
 three non-negative, period-separed integers [...]" *)
-let vo_magic = 8511
-let state_magic = 58511
+let vo_magic = 8591
+let state_magic = 58501
 let distributed_exec = ["coqtop";"coqc";"coqchk";"coqdoc";"coqmktop";"coqworkmgr";
 "coqdoc";"coq_makefile";"coq-tex";"gallina";"coqwc";"csdpcert"]
 
diff --git a/kernel/nativelib.mli b/kernel/nativelib.mli
index b4a3639f77..0941dc56ce 100644
--- a/kernel/nativelib.mli
+++ b/kernel/nativelib.mli
@@ -10,6 +10,9 @@ open Nativecode
 (** This file provides facilities to access OCaml compiler and dynamic linker,
 used by the native compiler. *)
 
+(* Directory where compiled files are stored *)
+val output_dir : string
+
 val get_load_paths : (unit -> string list) ref
 
 val load_obj : (string -> unit) ref
diff --git a/tools/coq_makefile.ml b/tools/coq_makefile.ml
index 28b86ddc78..e9bdb6caca 100644
--- a/tools/coq_makefile.ml
+++ b/tools/coq_makefile.ml
@@ -503,9 +503,9 @@ let parameters () =
   print "$(call includecmdwithout@,$(COQBIN)coqtop -config)\n\n";
   print "TIMED=\nTIMECMD=\nSTDTIME?=/usr/bin/time -f \"$* (user: %U mem: %M ko)\"\n";
   print "TIMER=$(if $(TIMED), $(STDTIME), $(TIMECMD))\n\n";
-  print "vo_to_obj = $(addsuffix .o,$(foreach vo,$(1),\\\n";
-  print "  $(addprefix $(dir $(vo)),$(addprefix .coq-native/,$(filter-out Warning: Error:,$(firstword \\\n";
-  print "    $(shell $(COQBIN)coqtop -q -noinit -batch -quiet -print-mod-uid $(vo))))))))\n\n"
+  print "vo_to_obj = $(addsuffix .o,\\\n";
+  print "  $(filter-out Warning: Error:,\\\n";
+  print "  $(shell $(COQBIN)coqtop -q -noinit -batch -quiet -print-mod-uid $(1))))\n\n"
 
 let include_dirs (inc_ml,inc_i,inc_r) =
   let parse_ml_includes l = List.map (fun (x,_) -> "-I \"" ^ x ^ "\"") l in
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index 9f670c7311..142f338674 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -375,9 +375,12 @@ let schedule_vio_compilation () =
   if !vio_files <> [] && not !vio_checking then
     Vio_checking.schedule_vio_compilation !vio_files_j !vio_files
 
-let print_native_name s =
+let get_native_name s =
   (* We ignore even critical errors because this mode has to be super silent *)
-  try print_endline (Library.native_name_from_filename s) with _ -> ()
+  try
+    String.concat Filename.dir_sep [Filename.dirname s;
+      Nativelib.output_dir; Library.native_name_from_filename s]
+  with _ -> ""
 
 let parse_args arglist =
   let args = ref arglist in
@@ -461,7 +464,7 @@ let parse_args arglist =
     |"-load-vernac-source"|"-l" -> add_load_vernacular false (next ())
     |"-load-vernac-source-verbose"|"-lv" -> add_load_vernacular true (next ())
     |"-outputstate" -> set_outputstate (next ())
-    |"-print-mod-uid" -> print_native_name (next ()); exit 0
+    |"-print-mod-uid" -> let s = String.concat " " (List.map get_native_name rem) in print_endline s; exit 0
     |"-require" -> add_require (next ())
     |"-top" -> set_toplevel_name (dirpath_of_string (next ()))
     |"-with-geoproof" -> Coq_config.with_geoproof := get_bool opt (next ())