diff options
| author | Emilio Jesus Gallego Arias | 2020-05-14 01:35:34 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2020-05-14 01:35:34 +0200 |
| commit | 2a43f3ef8e932f55a8f697ae24fef7075e62eb54 (patch) | |
| tree | befaf2a5c4a5df31f576226a2d5bb8e53761a090 /checker | |
| parent | 91b5990e724acc863a5dba66acc33fd698ac26f0 (diff) | |
| parent | 9e315837fded9763c3d7ca14a8aad0e7af3b4820 (diff) | |
Merge PR #12244: Store the OCaml version used for Coq in vo files.
Reviewed-by: ejgallego
Diffstat (limited to 'checker')
| -rw-r--r-- | checker/check.ml | 2 | ||||
| -rw-r--r-- | checker/values.ml | 2 |
2 files changed, 3 insertions, 1 deletions
diff --git a/checker/check.ml b/checker/check.ml index 31bfebc3d5..6d307b3c5e 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 () @@ -345,6 +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 + 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); diff --git a/checker/values.ml b/checker/values.ml index 76e3ab0d45..cce0ce7203 100644 --- a/checker/values.ml +++ b/checker/values.ml @@ -435,7 +435,7 @@ let v_stm_seg = v_pair v_tasks v_counters (** Toplevel structures in a vo (see Cic.mli) *) let v_libsum = - Tuple ("summary", [|v_dp;v_deps|]) + Tuple ("summary", [|v_dp;v_deps;String|]) let v_lib = Tuple ("library",[|v_compiled_lib;v_libraryobjs|]) |