From ac333e6297bd7c32282fa5f47bebeb35826072df Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Sat, 20 May 2017 01:24:46 +0200
Subject: [test-suite] Add tests for goal printing.

- https://coq.inria.fr/bugs/show_bug.cgi?id=5529
- https://coq.inria.fr/bugs/show_bug.cgi?id=5537

See also PR #640
---
 test-suite/output/goal_output.out |  8 ++++++++
 test-suite/output/goal_output.v   | 13 +++++++++++++
 2 files changed, 21 insertions(+)
 create mode 100644 test-suite/output/goal_output.out
 create mode 100644 test-suite/output/goal_output.v

diff --git a/test-suite/output/goal_output.out b/test-suite/output/goal_output.out
new file mode 100644
index 0000000000..773533a8d3
--- /dev/null
+++ b/test-suite/output/goal_output.out
@@ -0,0 +1,8 @@
+Nat.t = nat
+     : Set
+Nat.t = nat
+     : Set
+1 subgoal
+  
+  ============================
+  False
diff --git a/test-suite/output/goal_output.v b/test-suite/output/goal_output.v
new file mode 100644
index 0000000000..327b80b0aa
--- /dev/null
+++ b/test-suite/output/goal_output.v
@@ -0,0 +1,13 @@
+(* From
+   - https://coq.inria.fr/bugs/show_bug.cgi?id=5529
+   - https://coq.inria.fr/bugs/show_bug.cgi?id=5537
+ *)
+
+Print Nat.t.
+Timeout 1 Print Nat.t.
+
+Lemma toto: False.
+Set Printing All.
+Show.
+Abort.
+
-- 
cgit v1.2.3