From 763c71ec355b85ecfb8df3de07cce730f8947cb7 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Fri, 10 Jul 2020 18:41:30 +0200
Subject: Fix #12513: coq no longer reports mismatched version numbers.

---
 lib/objFile.ml | 2 +-
 lib/system.ml  | 7 +++++--
 2 files changed, 6 insertions(+), 3 deletions(-)

diff --git a/lib/objFile.ml b/lib/objFile.ml
index 96db51a010..26367aaffa 100644
--- a/lib/objFile.ml
+++ b/lib/objFile.ml
@@ -182,7 +182,7 @@ let open_in ~file =
     let version = input_int32 ch in
     let () =
       if not (Int32.equal magic magic_number) then
-        let e = { filename = file; actual = version; expected = magic_number } in
+        let e = { filename = file; actual = magic; expected = magic_number } in
         raise (Bad_magic_number e)
     in
     let () =
diff --git a/lib/system.ml b/lib/system.ml
index e25f758865..1aadaf6d3a 100644
--- a/lib/system.ml
+++ b/lib/system.ml
@@ -239,9 +239,12 @@ let intern_state magic filename =
 let with_magic_number_check f a =
   try f a
   with
-  | Bad_magic_number {filename=fname; _} ->
+  | Bad_magic_number {filename=fname; actual; expected} ->
     CErrors.user_err ~hdr:"with_magic_number_check"
-    (str"File " ++ str fname ++ strbrk" is corrupted.")
+    (str"File " ++ str fname ++ strbrk" has bad magic number " ++
+    (str @@ Int32.to_string actual) ++ str" (expected " ++ (str @@ Int32.to_string expected) ++ str")." ++
+    spc () ++
+    strbrk "It is corrupted or was compiled with another version of Coq.")
   | Bad_version_number {filename=fname;actual=actual;expected=expected} ->
     CErrors.user_err ~hdr:"with_magic_number_check"
     (str"File " ++ str fname ++ strbrk" has bad version number " ++
-- 
cgit v1.2.3


From e52f070515833634f7a52e3440be02229e71d4fb Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Fri, 10 Jul 2020 18:48:11 +0200
Subject: Add changelog.

---
 .../07-commands-and-options/12677-require-v811-error-compat.rst      | 5 +++++
 1 file changed, 5 insertions(+)
 create mode 100644 doc/changelog/07-commands-and-options/12677-require-v811-error-compat.rst

diff --git a/doc/changelog/07-commands-and-options/12677-require-v811-error-compat.rst b/doc/changelog/07-commands-and-options/12677-require-v811-error-compat.rst
new file mode 100644
index 0000000000..c654ddd69d
--- /dev/null
+++ b/doc/changelog/07-commands-and-options/12677-require-v811-error-compat.rst
@@ -0,0 +1,5 @@
+- **Fixed:**
+  Properly report the mismatched magic number of vo files
+  (`#12677 <https://github.com/coq/coq/pull/12677>`_,
+  fixes `#12513 <https://github.com/coq/coq/issues/12513>`_,
+  by Pierre-Marie Pédrot).
-- 
cgit v1.2.3