aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite
diff options
context:
space:
mode:
Diffstat (limited to 'test-suite')
-rw-r--r--test-suite/output/PrintAssumptions.out4
1 files changed, 2 insertions, 2 deletions
diff --git a/test-suite/output/PrintAssumptions.out b/test-suite/output/PrintAssumptions.out
index b3914a1cc..94d59a500 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