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 /checker | |
| parent | 3e04d6c024dd03878b0b487cf823f5586d6fd397 (diff) | |
Centralize the OCaml version-checking function.
We tweak the message a bit.
Diffstat (limited to 'checker')
| -rw-r--r-- | checker/check.ml | 9 |
1 files changed, 1 insertions, 8 deletions
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); |