From c101a710c96e03e228e4b1aacee8edebd3c8dabf Mon Sep 17 00:00:00 2001
From: xclerc
Date: Mon, 2 Dec 2013 13:08:55 +0100
Subject: Print logical name rather than path (thus allowing reproducible
 tests).

---
 library/library.ml                     | 9 +++++----
 test-suite/output/PrintAssumptions.out | 4 ++--
 2 files changed, 7 insertions(+), 6 deletions(-)

diff --git a/library/library.ml b/library/library.ml
index 1219fedec2..c3cc02fefe 100644
--- a/library/library.ml
+++ b/library/library.ml
@@ -280,11 +280,12 @@ exception Faulty
 (** Fetching a table of opaque terms at position [pos] in file [f],
     expecting to find first a copy of [digest]. *)
 
-let fetch_opaque_table (f,pos,digest) =
+let fetch_opaque_table dp (f,pos,digest) =
   if !Flags.load_proofs == Flags.Dont then
     error "Not accessing an opaque term due to option -dont-load-proofs.";
+  let dir_path = Names.DirPath.to_string dp in
   try
-    Pp.msg_info (Pp.str "Fetching opaque terms in " ++ str f);
+    Pp.msg_info (Pp.str "Fetching opaque terms from disk for " ++ str dir_path);
     let ch = System.with_magic_number_check raw_intern_library f in
     let () = seek_in ch pos in
     if not (String.equal (System.digest_in f ch) digest) then raise Faulty;
@@ -299,7 +300,7 @@ let fetch_opaque_table (f,pos,digest) =
     table
   with e when Errors.noncritical e ->
     error
-      ("The file "^f^" is inaccessible or corrupted,\n"
+      ("The file "^f^" (bound to " ^ dir_path ^ ") is inaccessible or corrupted,\n"
        ^ "cannot load some opaque constant bodies in it.\n")
 
 (** Delayed / available tables of opaque terms *)
@@ -317,7 +318,7 @@ let access_opaque_table dp i =
   let t = match LibraryMap.find dp !opaque_tables with
     | Fetched t -> t
     | ToFetch (f,pos,digest) ->
-      let t = fetch_opaque_table (f,pos,digest) in
+      let t = fetch_opaque_table dp (f,pos,digest) in
       add_opaque_table dp (Fetched t);
       t
   in
diff --git a/test-suite/output/PrintAssumptions.out b/test-suite/output/PrintAssumptions.out
index b3914a1cc4..94d59a5004 100644
--- a/test-suite/output/PrintAssumptions.out
+++ b/test-suite/output/PrintAssumptions.out
@@ -2,8 +2,8 @@ Axioms:
 foo : nat
 Axioms:
 foo : nat
-Fetching opaque terms in /home/pm/Desktop/sources/coq/theories/Arith/Plus.vo
-Fetching opaque terms in /home/pm/Desktop/sources/coq/theories/Init/Peano.vo
+Fetching opaque terms from disk for Coq.Arith.Plus
+Fetching opaque terms from disk for Coq.Init.Peano
 Axioms:
 extensionality : forall (P Q : Type) (f g : P -> Q),
                  (forall x : P, f x = g x) -> f = g
-- 
cgit v1.2.3