diff options
| author | Pierre-Marie Pédrot | 2020-05-13 12:55:19 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-05-13 13:01:28 +0200 |
| commit | 9e315837fded9763c3d7ca14a8aad0e7af3b4820 (patch) | |
| tree | de3f1189da6a868ae077c680fb14f2bca09d646c /lib/system.ml | |
| parent | 3e04d6c024dd03878b0b487cf823f5586d6fd397 (diff) | |
Centralize the OCaml version-checking function.
We tweak the message a bit.
Diffstat (limited to 'lib/system.ml')
| -rw-r--r-- | lib/system.ml | 9 |
1 files changed, 9 insertions, 0 deletions
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 |