diff options
| author | Enrico Tassi | 2019-10-30 10:25:39 +0100 |
|---|---|---|
| committer | Enrico Tassi | 2019-10-30 10:25:39 +0100 |
| commit | c09f318e200c57750fbefbce00e3f0c4d4ee2c97 (patch) | |
| tree | 6d1198af13ff2658432dcdae63349df9dd63d1d8 /test-suite | |
| parent | 99ed41bf8d6d72fc4d5a13d231663bbf48e9ec25 (diff) | |
| parent | 5ec7eca640a6ee495eb2c0fb8d8a4076256ff96d (diff) | |
Merge PR #10494: Show diffs in "Show Proof."
Reviewed-by: Zimmi48
Reviewed-by: gares
Ack-by: herbelin
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/output-coqtop/ShowProofDiffs.out | 42 | ||||
| -rw-r--r-- | test-suite/output-coqtop/ShowProofDiffs.v | 6 |
2 files changed, 48 insertions, 0 deletions
diff --git a/test-suite/output-coqtop/ShowProofDiffs.out b/test-suite/output-coqtop/ShowProofDiffs.out new file mode 100644 index 0000000000..285a3bcd89 --- /dev/null +++ b/test-suite/output-coqtop/ShowProofDiffs.out @@ -0,0 +1,42 @@ +
+Coq < Coq < 1 subgoal
+
+ ============================
+ [48;2;0;91;0m[48;2;0;141;0;4m[1mforall[22m i : nat, [37mexists[39m j k : nat[37m,[39m i[37m =[39m j[37m /\[39m j[37m =[39m k[37m /\[39m i[37m =[39m k[48;2;0;91;0;24m[0m
+
+x <
+x < 1 focused subgoal
+(shelved: 1)
+ [48;2;0;91;0m[48;2;0;141;0;4mi : nat[48;2;0;91;0;24m[0m
+ ============================
+ [48;2;0;91;0m[37mexists[39m k : nat[37m,[39m i[37m =[39m [48;2;0;141;0;4m[94m?[39m[48;2;0;91;0;24m[94mj[39m[37m /\[39m [48;2;0;141;0;4m[94m?[39m[48;2;0;91;0;24m[94mj[39m[37m =[39m k[37m /\[39m i[37m =[39m k[0m
+
+[48;2;0;91;0m[48;2;0;141;0;4m([1mfun[22m i : nat =>[49;24m
+ [48;2;0;141;0;4mex_intro ([1mfun[22m j : nat => [37mexists[39m k : nat[37m,[39m i[37m =[39m j[37m /\[39m j[37m =[39m k[37m /\[39m i[37m =[39m k) [94m?[39m[94mj[39m[48;2;0;91;0;24m ?Goal[48;2;0;141;0;4m)[48;2;0;91;0;24m[0m
+
+x < 1 focused subgoal
+(shelved: 2)
+ i : nat
+ ============================
+ [48;2;0;91;0mi[37m =[39m ?j[37m /\[39m ?j[37m =[39m [48;2;0;141;0;4m[94m?[39m[48;2;0;91;0;24m[94mk[39m[37m /\[39m i[37m =[39m [48;2;0;141;0;4m[94m?[39m[48;2;0;91;0;24m[94mk[39m[0m
+
+[48;2;0;91;0m([1mfun[22m i : nat =>[49m
+ [48;2;0;91;0mex_intro ([1mfun[22m j : nat => [37mexists[39m k : nat[37m,[39m i[37m =[39m j[37m /\[39m j[37m =[39m k[37m /\[39m i[37m =[39m k) [49m
+ [48;2;0;91;0m[48;2;0;141;0;4m[94m?[39m[94mj[39m (ex_intro ([1mfun[22m k : nat => i[37m =[39m ?j[37m /\[39m[48;2;0;91;0;24m ?j[37m [39m[48;2;0;141;0;4m[37m=[39m k[37m /\[39m i[37m =[39m k) [94m?[39m[94mk[39m[48;2;0;91;0;24m ?Goal[48;2;0;141;0;4m)[48;2;0;91;0;24m)[0m
+
+x < 2 focused subgoals
+(shelved: 2)
+ i : nat
+ ============================
+ [48;2;0;91;0mi[37m =[39m ?j[0m
+
+subgoal 2 is:
+ [48;2;0;91;0m?j[37m =[39m ?k[37m /\[39m i[37m =[39m ?k[0m
+
+[48;2;0;91;0m([1mfun[22m i : nat =>[49m
+ [48;2;0;91;0mex_intro ([1mfun[22m j : nat => [37mexists[39m k : nat[37m,[39m i[37m =[39m j[37m /\[39m j[37m =[39m k[37m /\[39m i[37m =[39m k) [49m
+ [48;2;0;91;0m?j[49m
+ [48;2;0;91;0m(ex_intro ([1mfun[22m k : nat => i[37m =[39m ?j[37m /\[39m ?j[37m =[39m k[37m /\[39m i[37m =[39m k) [49m
+ [48;2;0;91;0m?k [48;2;0;141;0;4m(conj[48;2;0;91;0;24m ?Goal [48;2;0;141;0;4m[94m?[39m[94mGoal0[39m)[48;2;0;91;0;24m))[0m
+
+x <
diff --git a/test-suite/output-coqtop/ShowProofDiffs.v b/test-suite/output-coqtop/ShowProofDiffs.v new file mode 100644 index 0000000000..4251c52cb4 --- /dev/null +++ b/test-suite/output-coqtop/ShowProofDiffs.v @@ -0,0 +1,6 @@ +(* coq-prog-args: ("-color" "on" "-diffs" "on") *) +Lemma x: forall(i : nat), exists(j k : nat), i = j /\ j = k /\ i = k. +Proof using. + eexists. Show Proof Diffs. + eexists. Show Proof Diffs. + split. Show Proof Diffs. |