From 9ca0e6ae17453fcd01f4bd319e544950ca4ec838 Mon Sep 17 00:00:00 2001
From: Pierre Boutillier
Date: Fri, 28 Feb 2014 12:06:56 +0100
Subject: test-suite: opaque term -> opaque proof

---
 test-suite/output/PrintAssumptions.out | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/test-suite/output/PrintAssumptions.out b/test-suite/output/PrintAssumptions.out
index 94d59a5004..253405b0f7 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 from disk for Coq.Arith.Plus
-Fetching opaque terms from disk for Coq.Init.Peano
+Fetching opaque proofs from disk for Coq.Arith.Plus
+Fetching opaque proofs 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