diff options
| author |  xclerc <xavier.clerc@inria.fr> | 2013-12-02 13:08:55 +0100 |
|---|---|---|
| committer | xclerc <xavier.clerc@inria.fr> | 2013-12-02 13:08:55 +0100 |
| commit | c101a710c96e03e228e4b1aacee8edebd3c8dabf (patch) | |
| tree | 76ddbd569d765018b8213889131cec64688506cd /test-suite/output/PrintAssumptions.out | |
| parent | 38ab183fa9c37e6e405db20ccc393465474a73c0 (diff) | |
Print logical name rather than path (thus allowing reproducible tests).
Diffstat (limited to 'test-suite/output/PrintAssumptions.out')
| -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 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 |