diff options
| author | Jim Fehrle | 2019-06-08 05:04:41 -0700 |
|---|---|---|
| committer | Jim Fehrle | 2019-06-25 12:45:03 -0700 |
| commit | 403917b7d9ecb2ddfaaac2185c355d415d5fa5bc (patch) | |
| tree | e5afcff136068558ac11b7643709be9a7710ebd5 /test-suite/output-coqtop | |
| parent | 7dfcb0f7c817e66280ab37b6c653b5596a16c249 (diff) | |
Re-add the "Show Goal" command for Prooftree in PG.
It prints a goal given its internal goal id and the Stm state id.
Diffstat (limited to 'test-suite/output-coqtop')
| -rw-r--r-- | test-suite/output-coqtop/ShowGoal.out | 73 | ||||
| -rw-r--r-- | test-suite/output-coqtop/ShowGoal.v | 11 |
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. |