From 1559f734060e49fe09d7221f63dd66e8e7d565a4 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Fri, 14 Oct 2016 20:17:48 +0200
Subject: Tests for info/debug auto/eauto.

This is while waiting for a deeper uniformization of auto, eauto, and
typeclasses eauto.

Incidentally includes a little fix in harmonizing auto/eauto printing.
---
 test-suite/output/auto.out | 20 ++++++++++++++++++++
 test-suite/output/auto.v   | 11 +++++++++++
 2 files changed, 31 insertions(+)
 create mode 100644 test-suite/output/auto.out
 create mode 100644 test-suite/output/auto.v

(limited to 'test-suite')

diff --git a/test-suite/output/auto.out b/test-suite/output/auto.out
new file mode 100644
index 0000000000..a5b55a9993
--- /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 0000000000..a77b7b82e6
--- /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.
-- 
cgit v1.2.3