diff options
| author | Emilio Jesus Gallego Arias | 2019-06-30 23:17:09 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2019-06-30 23:17:09 +0200 |
| commit | 82aa7ed1c929533f2b9e7acaa8264c5a81e7a45e (patch) | |
| tree | 5d33bce9bf95ea1812c2dc370c8d385bd7d5e774 /test-suite | |
| parent | 6d6b2d7132bc768783bad6738d778519c28c8f08 (diff) | |
| parent | 403917b7d9ecb2ddfaaac2185c355d415d5fa5bc (diff) | |
Merge PR #10356: Re-add the "Show Goal" command for Prooftree in PG.
Reviewed-by: Zimmi48
Reviewed-by: ejgallego
Reviewed-by: gares
Ack-by: herbelin
Ack-by: jfehrle
Diffstat (limited to 'test-suite')
| -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. |