diff options
| author | Emilio Jesus Gallego Arias | 2019-09-04 15:00:03 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2019-09-04 15:00:03 +0200 |
| commit | 6a6a2575c10d05cd0151a83c133825d43bd3cb28 (patch) | |
| tree | a46211ebfa7af615d7edd8359208f8e5dcd5af1d /test-suite | |
| parent | bcf2dae1e39c6ff27c574a82c4451323a673b15f (diff) | |
| parent | 2d4033152c51eb0b093c79d19a5146995af1b432 (diff) | |
Merge PR #10612: Fix feedback levels
Ack-by: ejgallego
Reviewed-by: gares
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/output/auto.out | 16 |
1 files changed, 8 insertions, 8 deletions
diff --git a/test-suite/output/auto.out b/test-suite/output/auto.out index 2761b87b02..5e81b43504 100644 --- a/test-suite/output/auto.out +++ b/test-suite/output/auto.out @@ -2,18 +2,18 @@ simple apply or_intror (in core). intro. assumption. -Debug: (* debug auto: *) -Debug: * assumption. (*fail*) -Debug: * intro. (*fail*) -Debug: * simple apply or_intror (in core). (*success*) -Debug: ** assumption. (*fail*) -Debug: ** intro. (*success*) -Debug: ** assumption. (*success*) +(* debug auto: *) +* assumption. (*fail*) +* intro. (*fail*) +* simple apply or_intror (in core). (*success*) +** assumption. (*fail*) +** intro. (*success*) +** assumption. (*success*) (* info eauto: *) simple apply or_intror. intro. exact H. -Debug: (* debug eauto: *) +(* debug eauto: *) Debug: 1 depth=5 Debug: 1.1 depth=4 simple apply or_intror Debug: 1.1.1 depth=4 intro |