Merge remote-tracking branch 'forge/v8.5'

3 files changed, 29 insertions, 13 deletions

diff --git a/kernel/byterun/coq_gc.h b/kernel/byterun/coq_gc.h
index c7b18b900..f06275862 100644
--- a/kernel/byterun/coq_gc.h
+++ b/kernel/byterun/coq_gc.h
@@ -12,6 +12,7 @@
 #define _COQ_CAML_GC_
 #include <caml/mlvalues.h>
 #include <caml/alloc.h>
+#include <caml/memory.h>
 
 typedef void (*scanning_action) (value, value *);
 
@@ -24,12 +25,22 @@ CAMLextern void minor_collection (void);
 #define Caml_white (0 << 8)
 #define Caml_black (3 << 8)
 
+#ifdef HAS_OCP_MEMPROF
+
+/*  This code is necessary to make the OCamlPro memory profiling branch of
+    OCaml compile. */
+
+#define Make_header(wosize, tag, color)                                 \
+  caml_make_header(wosize, tag, color)
+
+#else
+
 #define Make_header(wosize, tag, color)                                 \
   (((header_t) (((header_t) (wosize) << 10)                             \
 		+ (color)                                               \
 		+ (tag_t) (tag)))   					\
    )
-
+#endif
 
 #define Alloc_small(result, wosize, tag) do{                            \
   young_ptr -= Bhsize_wosize (wosize);                                  \
diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml
index ada7ae737..f56b6f83e 100644
--- a/kernel/nativecode.ml
+++ b/kernel/nativecode.ml
@@ -2015,9 +2015,13 @@ let rec compile_deps env sigma prefix ~interactive init t =
         || (Cmap_env.mem c const_updates)
       then init
       else
-      let comp_stack, (mind_updates, const_updates) = match cb.const_body with
-        | Def t ->
+      let comp_stack, (mind_updates, const_updates) =
+	match cb.const_proj, cb.const_body with
+        | None, Def t ->
 	   compile_deps env sigma prefix ~interactive init (Mod_subst.force_constr t)
+	| Some pb, _ ->
+	   let mind = pb.proj_ind in
+	   compile_mind_deps env prefix ~interactive init mind
         | _ -> init
       in
       let code, name =
diff --git a/kernel/nativelib.ml b/kernel/nativelib.ml
index 4be8ced54..ce9e4e2b0 100644
--- a/kernel/nativelib.ml
+++ b/kernel/nativelib.ml
@@ -102,22 +102,23 @@ let compile_library dir code fn =
   r
 
 (* call_linker links dynamically the code for constants in environment or a  *)
-(* conversion test. Silently fails if the file does not exist in bytecode    *)
-(* mode, since the standard library is not compiled to bytecode with default *)
-(* settings.                                                                 *)
+(* conversion test. *)
 let call_linker ?(fatal=true) prefix f upds =
   rt1 := dummy_value ();
   rt2 := dummy_value ();
-  if Dynlink.is_native || Sys.file_exists f then
+  if not (Sys.file_exists f) then
+    let msg = "Cannot find native compiler file " ^ f in
+    if fatal then Errors.error msg
+    else Pp.msg_warning (Pp.str msg)
+  else
   (try
     if Dynlink.is_native then Dynlink.loadfile f else !load_obj f;
     register_native_file prefix
-   with | Dynlink.Error e ->
-          let msg = "Dynlink error, " ^ Dynlink.error_message e in
-          if fatal then anomaly (Pp.str msg) else Pp.msg_warning (Pp.str msg)
-        | e when Errors.noncritical e ->
-          if fatal then anomaly (Errors.print e)
-	  else Pp.msg_warning (Errors.print_no_report e));
+   with Dynlink.Error e as exn ->
+     let exn = Errors.push exn in
+     let msg = "Dynlink error, " ^ Dynlink.error_message e in
+     if fatal then (Pp.msg_error (Pp.str msg); iraise exn)
+     else Pp.msg_warning (Pp.str msg));
   match upds with Some upds -> update_locations upds | _ -> ()
 
 let link_library ~prefix ~dirname ~basename =