diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2015-09-03 20:50:31 +0200 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2015-09-03 20:50:31 +0200 |
| commit | 26be4ca94f8ba0a03826a2df09491bb0d96d7363 (patch) | |
| tree | 57a58d90386e19f92114ad4c9f1598b773592f02 /test-suite/output/PrintAssumptions.out | |
| parent | 6000ddffed48b804669a5eae9be7c536bf5e19c5 (diff) | |
Update test-suite after 518049fe7.
"Fetching opaque proofs" notices are not printed by default anymore.
Diffstat (limited to 'test-suite/output/PrintAssumptions.out')
| -rw-r--r-- | test-suite/output/PrintAssumptions.out | 5 |
1 files changed, 0 insertions, 5 deletions
diff --git a/test-suite/output/PrintAssumptions.out b/test-suite/output/PrintAssumptions.out index 08df91507..23f33081b 100644 --- a/test-suite/output/PrintAssumptions.out +++ b/test-suite/output/PrintAssumptions.out @@ -2,11 +2,6 @@ Axioms: foo : nat Axioms: foo : nat -Fetching opaque proofs from disk for Coq.Numbers.NatInt.NZAdd -Fetching opaque proofs from disk for Coq.Arith.PeanoNat -Fetching opaque proofs from disk for Coq.Classes.Morphisms -Fetching opaque proofs from disk for Coq.Init.Logic -Fetching opaque proofs from disk for Coq.Numbers.NatInt.NZBase Axioms: extensionality : forall (P Q : Type) (f g : P -> Q), (forall x : P, f x = g x) -> f = g |