From 9e315837fded9763c3d7ca14a8aad0e7af3b4820 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Wed, 13 May 2020 12:55:19 +0200
Subject: Centralize the OCaml version-checking function.

We tweak the message a bit.
---
 checker/check.ml | 9 +--------
 1 file changed, 1 insertion(+), 8 deletions(-)

(limited to 'checker')

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);
-- 
cgit v1.2.3