aboutsummaryrefslogtreecommitdiff
path: root/test-suite
diff options
context:
space:
mode:
authorcoqbot-app[bot]2020-10-12 16:34:24 +0000
committerGitHub2020-10-12 16:34:24 +0000
commit2ff70d8341177d384043dd3d02da6968a8788e32 (patch)
tree185a87d93ba54cbea6df675c4ec095fe873a5215 /test-suite
parent60e8fa2c4120a1f95e873c49929f4b879a814ddd (diff)
parent1d4bbefe5fe19306ab415e537863763a0a74134a (diff)
Merge PR #12874: Add a "Show Proof Diffs" message to the XML protocol
Reviewed-by: herbelin Ack-by: gares Ack-by: ejgallego
Diffstat (limited to 'test-suite')
-rw-r--r--test-suite/ide/proof-diffs.fake10
1 files changed, 10 insertions, 0 deletions
diff --git a/test-suite/ide/proof-diffs.fake b/test-suite/ide/proof-diffs.fake
new file mode 100644
index 0000000000..594ebced23
--- /dev/null
+++ b/test-suite/ide/proof-diffs.fake
@@ -0,0 +1,10 @@
+ADD { Goal True /\ False /\ True = False. }
+ADD { split. }
+GOALS
+ADD here { split. }
+GOALS
+PDIFF here
+ADD there { auto. }
+GOALS
+PDIFF there
+ADD { Admitted. }