From 9d319872a1668775ba1d72ae856f46fd7f082bb9 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Fri, 28 Aug 2020 15:15:00 +0200
Subject: par: print relevant subgoal when failing

Fix (partial) #5502
---
 test-suite/output/Partac.out | 6 ++++++
 test-suite/output/Partac.v   | 6 ++++++
 2 files changed, 12 insertions(+)
 create mode 100644 test-suite/output/Partac.out
 create mode 100644 test-suite/output/Partac.v

(limited to 'test-suite')

diff --git a/test-suite/output/Partac.out b/test-suite/output/Partac.out
new file mode 100644
index 0000000000..889e698fa2
--- /dev/null
+++ b/test-suite/output/Partac.out
@@ -0,0 +1,6 @@
+The command has indeed failed with message:
+The term "false" has type "bool" while it is expected to have type "nat".
+(for subgoal 1)
+The command has indeed failed with message:
+The term "0" has type "nat" while it is expected to have type "bool".
+(for subgoal 2)
diff --git a/test-suite/output/Partac.v b/test-suite/output/Partac.v
new file mode 100644
index 0000000000..f579ee683b
--- /dev/null
+++ b/test-suite/output/Partac.v
@@ -0,0 +1,6 @@
+Goal nat * bool.
+Proof.
+  split.
+  Fail par: exact false.
+  Fail par: exact 0.
+Abort.
-- 
cgit v1.2.3