Store the OCaml version used for Coq in vo files.

1 files changed, 12 insertions, 0 deletions

diff --git a/vernac/library.ml b/vernac/library.ml
index 85db501e84..2cd642c7e8 100644
--- a/vernac/library.ml
+++ b/vernac/library.ml
@@ -89,6 +89,7 @@ type library_disk = {
 type summary_disk = {
   md_name : compilation_unit_name;
   md_deps : (compilation_unit_name * Safe_typing.vodigest) array;
+  md_ocaml : string;
 }
 
 (*s Modules loaded in memory contain the following informations. They are
@@ -244,6 +245,14 @@ let mk_summary m = {
   libsum_digests = m.library_digests;
 }
 
+let check_ocaml_version num f =
+  if not (String.equal num Coq_config.caml_version) then
+  user_err Pp.(
+    str ("The file " ^ f ^ " was compiled with OCaml") ++ spc () ++
+    str num ++ spc () ++ str "while this instance of Coq was compiled with OCaml" ++
+    spc () ++ str Coq_config.caml_version
+  )
+
 let intern_from_file f =
   let ch = raw_intern_library f in
   let (lsd : seg_sum), digest_lsd = ObjFile.marshal_in_segment ch ~segment:"summary" in
@@ -251,6 +260,7 @@ let intern_from_file f =
   let (univs : seg_univ option), digest_u = ObjFile.marshal_in_segment ch ~segment:"universes" in
   let ((del_opaque : seg_proofs delayed),_) = in_delayed f ch ~segment:"opaques" in
   ObjFile.close_in ch;
+  check_ocaml_version lsd.md_ocaml f;
   register_library_filename lsd.md_name f;
   add_opaque_table lsd.md_name (ToFetch del_opaque);
   let open Safe_typing in
@@ -401,6 +411,7 @@ let load_library_todo f =
   let tasks, _ = ObjFile.marshal_in_segment ch ~segment:"tasks" in
   let (s4 : seg_proofs), _ = ObjFile.marshal_in_segment ch ~segment:"opaques" in
   ObjFile.close_in ch;
+  check_ocaml_version s0.md_ocaml f;
   if tasks = None then user_err ~hdr:"restart" (str"not a .vio file");
   if s2 = None then user_err ~hdr:"restart" (str"not a .vio file");
   if snd (Option.get s2) then user_err ~hdr:"restart" (str"not a .vio file");
@@ -486,6 +497,7 @@ let save_library_to todo_proofs ~output_native_objects dir f otab =
     let sd = {
     md_name = dir;
     md_deps = Array.of_list (current_deps ());
+    md_ocaml = Coq_config.caml_version;
   } in
   let md = {
     md_compiled = cenv;