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/system.ml | 7 +++++--
 1 file changed, 5 insertions(+), 2 deletions(-)

(limited to 'lib/system.ml')

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