Centralize the OCaml version-checking function.

We tweak the message a bit.

1 files changed, 2 insertions, 10 deletions

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");