Merge PR #9898: Better error message when OCaml compiler not found for native compute

Reviewed-by: ejgallego

1 files changed, 9 insertions, 14 deletions

diff --git a/kernel/nativeconv.ml b/kernel/nativeconv.ml
index baa290367f..d153f84e9c 100644
--- a/kernel/nativeconv.ml
+++ b/kernel/nativeconv.ml
@@ -8,7 +8,6 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
-open CErrors
 open Names
 open Nativelib
 open Reduction
@@ -152,19 +151,15 @@ let native_conv_gen pb sigma env univs t1 t2 =
   else
   let ml_filename, prefix = get_ml_filename () in
   let code, upds = mk_conv_code env sigma prefix t1 t2 in
-  match compile ml_filename code ~profile:false with
-  | (true, fn) ->
-      begin
-        if !Flags.debug then Feedback.msg_debug (Pp.str "Running test...");
-        let t0 = Sys.time () in
-        call_linker ~fatal:true prefix fn (Some upds);
-        let t1 = Sys.time () in
-        let time_info = Format.sprintf "Evaluation done in %.5f@." (t1 -. t0) in
-        if !Flags.debug then Feedback.msg_debug (Pp.str time_info);
-        (* TODO change 0 when we can have de Bruijn *)
-        fst (conv_val env pb 0 !rt1 !rt2 univs)
-      end
-  | _ -> anomaly (Pp.str "Compilation failure.") 
+  let fn = compile ml_filename code ~profile:false in
+  if !Flags.debug then Feedback.msg_debug (Pp.str "Running test...");
+  let t0 = Sys.time () in
+  call_linker ~fatal:true prefix fn (Some upds);
+  let t1 = Sys.time () in
+  let time_info = Format.sprintf "Evaluation done in %.5f@." (t1 -. t0) in
+  if !Flags.debug then Feedback.msg_debug (Pp.str time_info);
+  (* TODO change 0 when we can have de Bruijn *)
+  fst (conv_val env pb 0 !rt1 !rt2 univs)
 
 (* Wrapper for [native_conv] above *)
 let native_conv cv_pb sigma env t1 t2 =