aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite
diff options
context:
space:
mode:
Diffstat (limited to 'test-suite')
-rw-r--r--test-suite/output/auto.out20
-rw-r--r--test-suite/output/auto.v11
2 files changed, 31 insertions, 0 deletions
diff --git a/test-suite/output/auto.out b/test-suite/output/auto.out
new file mode 100644
index 000000000..a5b55a999
--- /dev/null
+++ b/test-suite/output/auto.out
@@ -0,0 +1,20 @@
+(* info auto: *)
+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*)
+(* info eauto: *)
+simple apply or_intror.
+ intro.
+ exact H.
+Debug: (* debug eauto: *)
+Debug: 1 depth=5
+Debug: 1.1 depth=4 simple apply or_intror
+Debug: 1.1.1 depth=4 intro
+Debug: 1.1.1.1 depth=4 exact H
diff --git a/test-suite/output/auto.v b/test-suite/output/auto.v
new file mode 100644
index 000000000..a77b7b82e
--- /dev/null
+++ b/test-suite/output/auto.v
@@ -0,0 +1,11 @@
+(* testing info/debug auto/eauto *)
+
+Goal False \/ (True -> True).
+info_auto.
+Undo.
+debug auto.
+Undo.
+info_eauto.
+Undo.
+debug eauto.
+Qed.