diff options
| author |  Pierre Boutillier <pierre.boutillier@ens-lyon.org> | 2014-02-28 12:06:56 +0100 |
|---|---|---|
| committer | Pierre Boutillier <pierre.boutillier@ens-lyon.org> | 2014-02-28 17:29:13 +0100 |
| commit | 9ca0e6ae17453fcd01f4bd319e544950ca4ec838 (patch) | |
| tree | 4f7cbe8fa80aa293174b890aa956a73f1119e0ef | |
| parent | cc06ffe3df0ecc023ad046a085b0751ed4161cbf (diff) | |
test-suite: opaque term -> opaque proof
| -rw-r--r-- | test-suite/output/PrintAssumptions.out | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/test-suite/output/PrintAssumptions.out b/test-suite/output/PrintAssumptions.out index 94d59a500..253405b0f 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 |