diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-07-21 18:20:25 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-07-21 18:23:03 +0200 |
| commit | 99efd521c3bd01f885248f6ac03c450e98929b2e (patch) | |
| tree | 0170bfde075802d0206d5b098019e792bbe01cc9 /test-suite/output/PrintAssumptions.out | |
| parent | 783b0af48fc24a2181d960d034d959f265b5d604 (diff) | |
Fixing output test-suite.
Diffstat (limited to 'test-suite/output/PrintAssumptions.out')
| -rw-r--r-- | test-suite/output/PrintAssumptions.out | 7 |
1 files changed, 5 insertions, 2 deletions
diff --git a/test-suite/output/PrintAssumptions.out b/test-suite/output/PrintAssumptions.out index 253405b0f..08df91507 100644 --- a/test-suite/output/PrintAssumptions.out +++ b/test-suite/output/PrintAssumptions.out @@ -2,8 +2,11 @@ Axioms: foo : nat Axioms: foo : nat -Fetching opaque proofs from disk for Coq.Arith.Plus -Fetching opaque proofs from disk for Coq.Init.Peano +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 |