diff options
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/system.ml | 9 | ||||
| -rw-r--r-- | lib/system.mli | 2 |
2 files changed, 11 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 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 |