diff options
| author | Pierre-Marie Pédrot | 2020-05-03 20:34:41 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-05-13 12:50:41 +0200 |
| commit | 3e04d6c024dd03878b0b487cf823f5586d6fd397 (patch) | |
| tree | 4be4f12a7979e1ed44d44b011feac7f770df81aa /checker/check.ml | |
| parent | 67f0e9fd40dc2f7b30a8aec4c7efb032e61a001e (diff) | |
Store the OCaml version used for Coq in vo files.
Diffstat (limited to 'checker/check.ml')
| -rw-r--r-- | checker/check.ml | 9 |
1 files changed, 9 insertions, 0 deletions
diff --git a/checker/check.ml b/checker/check.ml index 31bfebc3d5..26de2db109 100644 --- a/checker/check.ml +++ b/checker/check.ml @@ -263,6 +263,7 @@ let raw_intern_library f = type summary_disk = { md_name : compilation_unit_name; md_deps : (compilation_unit_name * Safe_typing.vodigest) array; + md_ocaml : string; } module Dyn = Dyn.Make () @@ -289,6 +290,11 @@ 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 *) @@ -345,6 +351,9 @@ 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); if dir <> sd.md_name then user_err ~hdr:"intern_from_file" (name_clash_message dir sd.md_name f); |