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.
---
 lib/system.ml | 9 +++++++++
 1 file changed, 9 insertions(+)

(limited to 'lib/system.ml')

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