From 5ec7eca640a6ee495eb2c0fb8d8a4076256ff96d Mon Sep 17 00:00:00 2001
From: Jim Fehrle
Date: Sat, 6 Jul 2019 19:25:39 -0700
Subject: Show diffs in "Show Proof."

Add experimental "Show Proof" command to the toplevel that shadows
the current command in the parser (in coqtop and PG only).
Apply existing code to highlight diffs in the output
---
 test-suite/output-coqtop/ShowProofDiffs.out | 42 +++++++++++++++++++++++++++++
 test-suite/output-coqtop/ShowProofDiffs.v   |  6 +++++
 2 files changed, 48 insertions(+)
 create mode 100644 test-suite/output-coqtop/ShowProofDiffs.out
 create mode 100644 test-suite/output-coqtop/ShowProofDiffs.v

(limited to 'test-suite')

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
+  
+  ============================
+  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
+
+(fun i : nat =>
+ ex_intro (fun j : nat => exists k : nat, i = j /\ j = k /\ i = k) ?j ?Goal)
+
+x < 1 focused subgoal
+(shelved: 2)
+  i : nat
+  ============================
+  i = ?j /\ ?j = ?k /\ i = ?k
+
+(fun i : nat =>
+ ex_intro (fun j : nat => exists k : nat, i = j /\ j = k /\ i = k) 
+   ?j (ex_intro (fun k : nat => i = ?j /\ ?j = k /\ i = k) ?k ?Goal))
+
+x < 2 focused subgoals
+(shelved: 2)
+  i : nat
+  ============================
+  i = ?j
+
+subgoal 2 is:
+ ?j = ?k /\ i = ?k
+
+(fun i : nat =>
+ ex_intro (fun j : nat => exists k : nat, i = j /\ j = k /\ i = k) 
+   ?j
+   (ex_intro (fun k : nat => i = ?j /\ ?j = k /\ i = k) 
+      ?k (conj ?Goal ?Goal0)))
+
+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.
-- 
cgit v1.2.3