From c3dc9c558be3d3fe532d3bb3de747e920ce3e47b Mon Sep 17 00:00:00 2001
From: Attila Gáspár
Date: Sat, 6 Jun 2020 15:29:46 +0200
Subject: Fix #12442: Confusing error message when the intro pattern of "apply
 in" fails

---
 test-suite/output/bug12442.out |  6 ++++++
 test-suite/output/bug12442.v   | 10 ++++++++++
 2 files changed, 16 insertions(+)
 create mode 100644 test-suite/output/bug12442.out
 create mode 100644 test-suite/output/bug12442.v

(limited to 'test-suite')

diff --git a/test-suite/output/bug12442.out b/test-suite/output/bug12442.out
new file mode 100644
index 0000000000..644ef6cd7c
--- /dev/null
+++ b/test-suite/output/bug12442.out
@@ -0,0 +1,6 @@
+The command has indeed failed with message:
+No product even after head-reduction.
+The command has indeed failed with message:
+Not an inductive product.
+The command has indeed failed with message:
+Not an inductive product.
diff --git a/test-suite/output/bug12442.v b/test-suite/output/bug12442.v
new file mode 100644
index 0000000000..481989a4e9
--- /dev/null
+++ b/test-suite/output/bug12442.v
@@ -0,0 +1,10 @@
+Parameter A B : Prop.
+Axiom P : inhabited (A -> B).
+
+Goal A -> True.
+Proof.
+  Fail intros ?%P ?.
+  Fail intros []%P.
+  intro a.
+  Fail apply P in a as [].
+Abort.
-- 
cgit v1.2.3