From 403917b7d9ecb2ddfaaac2185c355d415d5fa5bc Mon Sep 17 00:00:00 2001
From: Jim Fehrle
Date: Sat, 8 Jun 2019 05:04:41 -0700
Subject: Re-add the "Show Goal" command for Prooftree in PG. It prints a goal
 given its internal goal id and the Stm state id.

---
 test-suite/output-coqtop/ShowGoal.out | 73 +++++++++++++++++++++++++++++++++++
 test-suite/output-coqtop/ShowGoal.v   | 11 ++++++
 2 files changed, 84 insertions(+)
 create mode 100644 test-suite/output-coqtop/ShowGoal.out
 create mode 100644 test-suite/output-coqtop/ShowGoal.v

(limited to 'test-suite')

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.
-- 
cgit v1.2.3