2 files changed, 84 insertions, 0 deletions
diff --git a/test-suite/output-coqtop/ShowGoal.out b/test-suite/output-coqtop/ShowGoal.out
new file mode 100644
index 0000000000..2eadd22db8
--- /dev/null
+++ b/test-suite/output-coqtop/ShowGoal.out
@@ -0,0 +1,73 @@
+
+Coq < 1 subgoal
+  
+  ============================
+  forall i : nat, exists j k : nat, i = j /\ j = k /\ i = k
+
+x < 
+x < 1 focused subgoal
+(shelved: 1)
+  
+  i : nat
+  ============================
+  exists k : nat, i = ?j /\ ?j = k /\ i = k
+
+x < 1 focused subgoal
+(shelved: 2)
+  
+  i : nat
+  ============================
+  i = ?j /\ ?j = ?k /\ i = ?k
+
+x < 2 focused subgoals
+(shelved: 2)
+  
+  i : nat
+  ============================
+  i = ?j
+
+subgoal 2 is:
+ ?j = ?k /\ i = ?k
+
+x < 1 focused subgoal
+(shelved: 1)
+  
+  i : nat
+  ============================
+  i = ?k /\ i = ?k
+
+x < 2 focused subgoals
+(shelved: 1)
+  
+  i : nat
+  ============================
+  i = ?k
+
+subgoal 2 is:
+ i = ?k
+
+x < 1 subgoal
+  
+  i : nat
+  ============================
+  i = i
+
+x < goal ID 16 at state 5
+  
+  i : nat
+  ============================
+  i = ?j /\ ?j = ?k /\ i = ?k
+
+x < goal ID 16 at state 7
+  
+  i : nat
+  ============================
+  i = i /\ i = ?k /\ i = ?k
+
+x < goal ID 16 at state 9
+  
+  i : nat
+  ============================
+  i = i /\ i = i /\ i = i
+
+x < 
diff --git a/test-suite/output-coqtop/ShowGoal.v b/test-suite/output-coqtop/ShowGoal.v
new file mode 100644
index 0000000000..9545254770
--- /dev/null
+++ b/test-suite/output-coqtop/ShowGoal.v
@@ -0,0 +1,11 @@
+Lemma x: forall(i : nat), exists(j k : nat), i = j /\ j = k /\ i = k.
+Proof using.
+  eexists.
+  eexists.
+  split.
+    trivial.
+  split.
+    trivial.
+Show Goal 16 at 5.
+Show Goal 16 at 7.
+Show Goal 16 at 9.