Centralize the OCaml version-checking function.

We tweak the message a bit.

4 files changed, 14 insertions, 18 deletions

diff --git a/checker/check.ml b/checker/check.ml
index 26de2db109..6d307b3c5e 100644
--- a/checker/check.ml
+++ b/checker/check.ml
@@ -290,11 +290,6 @@ let name_clash_message dir mdir f =
   pr_dirpath mdir ++ spc () ++ str "and not library" ++ spc() ++
   pr_dirpath dir
 
-let caml_version_mismatch s f =
-  str ("The file " ^ f ^ " was compiled with OCaml") ++ spc () ++
-  str s ++ spc () ++ str "while this instance of Coq was compiled with OCaml" ++
-  spc() ++ str Coq_config.caml_version
-
 type intern_mode = Rec | Root | Dep (* Rec = standard, Root = -norec, Dep = dependency of norec *)
 
 (* Dependency graph *)
@@ -351,9 +346,7 @@ let intern_from_file ~intern_mode (dir, f) =
       let () = close_in ch in
       let ch = open_in_bin f in
       let () = close_in ch in
-      if Coq_config.caml_version <> sd.md_ocaml then
-        user_err ~hdr:"intern_from_file"
-          (caml_version_mismatch sd.md_ocaml f);
+      let () = System.check_caml_version ~caml:sd.md_ocaml ~file:f in
       if dir <> sd.md_name then
         user_err ~hdr:"intern_from_file"
           (name_clash_message dir sd.md_name f);
diff --git a/lib/system.ml b/lib/system.ml
index 4e98651d6e..e25f758865 100644
--- a/lib/system.ml
+++ b/lib/system.ml
@@ -168,6 +168,15 @@ let try_remove filename =
 let error_corrupted file s =
   CErrors.user_err ~hdr:"System" (str file ++ str ": " ++ str s ++ str ". Try to rebuild it.")
 
+let check_caml_version ~caml:s ~file:f =
+  if not (String.equal Coq_config.caml_version s) then
+    CErrors.user_err (str ("The file " ^ f ^ " was compiled with OCaml") ++
+    spc () ++ str s ++ spc () ++ str "while this instance of Coq was compiled \
+    with OCaml" ++ spc() ++ str Coq_config.caml_version ++ str "." ++ spc () ++
+    str "Coq object files need to be compiled with the same OCaml toolchain to \
+    be compatible.")
+  else ()
+
 let input_binary_int f ch =
   try input_binary_int ch
   with
diff --git a/lib/system.mli b/lib/system.mli
index 4a8c35b6ea..1e2f519327 100644
--- a/lib/system.mli
+++ b/lib/system.mli
@@ -88,6 +88,8 @@ val with_magic_number_check : ('a -> 'b) -> 'a -> 'b
 val marshal_out : out_channel -> 'a -> unit
 val marshal_in : string -> in_channel -> 'a
 
+val check_caml_version : caml:string -> file:string -> unit
+
 (** {6 Time stamps.} *)
 
 type time
diff --git a/vernac/library.ml b/vernac/library.ml
index 2cd642c7e8..c30331b221 100644
--- a/vernac/library.ml
+++ b/vernac/library.ml
@@ -245,14 +245,6 @@ let mk_summary m = {
   libsum_digests = m.library_digests;
 }
 
-let check_ocaml_version num f =
-  if not (String.equal num Coq_config.caml_version) then
-  user_err Pp.(
-    str ("The file " ^ f ^ " was compiled with OCaml") ++ spc () ++
-    str num ++ spc () ++ str "while this instance of Coq was compiled with OCaml" ++
-    spc () ++ str Coq_config.caml_version
-  )
-
 let intern_from_file f =
   let ch = raw_intern_library f in
   let (lsd : seg_sum), digest_lsd = ObjFile.marshal_in_segment ch ~segment:"summary" in
@@ -260,7 +252,7 @@ let intern_from_file f =
   let (univs : seg_univ option), digest_u = ObjFile.marshal_in_segment ch ~segment:"universes" in
   let ((del_opaque : seg_proofs delayed),_) = in_delayed f ch ~segment:"opaques" in
   ObjFile.close_in ch;
-  check_ocaml_version lsd.md_ocaml f;
+  System.check_caml_version ~caml:lsd.md_ocaml ~file:f;
   register_library_filename lsd.md_name f;
   add_opaque_table lsd.md_name (ToFetch del_opaque);
   let open Safe_typing in
@@ -411,7 +403,7 @@ let load_library_todo f =
   let tasks, _ = ObjFile.marshal_in_segment ch ~segment:"tasks" in
   let (s4 : seg_proofs), _ = ObjFile.marshal_in_segment ch ~segment:"opaques" in
   ObjFile.close_in ch;
-  check_ocaml_version s0.md_ocaml f;
+  System.check_caml_version ~caml:s0.md_ocaml ~file:f;
   if tasks = None then user_err ~hdr:"restart" (str"not a .vio file");
   if s2 = None then user_err ~hdr:"restart" (str"not a .vio file");
   if snd (Option.get s2) then user_err ~hdr:"restart" (str"not a .vio file");