Catch errors while coercing 'and' intro patterns

Fixes GH#6384 and GH#6385.

4 files changed, 44 insertions, 0 deletions

diff --git a/test-suite/bugs/closed/gh6384.v b/test-suite/bugs/closed/gh6384.v
new file mode 100644
index 0000000000..cec84642fb
--- /dev/null
+++ b/test-suite/bugs/closed/gh6384.v
@@ -0,0 +1,5 @@
+Theorem test (A:Prop) : A \/ A -> A.
+  Fail intro H; destruct H as H.
+  (* Error: Disjunctive/conjunctive introduction pattern expected. *)
+  Fail intros H; destruct H as H.
+Abort.
diff --git a/test-suite/bugs/closed/gh6385.v b/test-suite/bugs/closed/gh6385.v
new file mode 100644
index 0000000000..3bbb664f4f
--- /dev/null
+++ b/test-suite/bugs/closed/gh6385.v
@@ -0,0 +1,5 @@
+Theorem test (A:Prop) : A \/ A -> A.
+  Fail let H := idtac in intros H; destruct H as H'.
+  (* Disjunctive/conjunctive introduction pattern expected. *)
+  Fail let H' := idtac in intros H; destruct H as H'.
+Abort.
diff --git a/test-suite/output/InvalidDisjunctiveIntro.out b/test-suite/output/InvalidDisjunctiveIntro.out
new file mode 100644
index 0000000000..25a306b458
--- /dev/null
+++ b/test-suite/output/InvalidDisjunctiveIntro.out
@@ -0,0 +1,16 @@
+The command has indeed failed with message:
+Cannot coerce to a disjunctive/conjunctive pattern.
+The command has indeed failed with message:
+Disjunctive/conjunctive introduction pattern expected.
+The command has indeed failed with message:
+Cannot coerce to a disjunctive/conjunctive pattern.
+The command has indeed failed with message:
+Cannot coerce to a disjunctive/conjunctive pattern.
+The command has indeed failed with message:
+Ltac variable H is bound to <tactic closure> which cannot be coerced to
+an introduction pattern.
+The command has indeed failed with message:
+Disjunctive/conjunctive introduction pattern expected.
+The command has indeed failed with message:
+Ltac variable H' is bound to <tactic closure> which cannot be coerced to
+an introduction pattern.
diff --git a/test-suite/output/InvalidDisjunctiveIntro.v b/test-suite/output/InvalidDisjunctiveIntro.v
new file mode 100644
index 0000000000..4febdf0344
--- /dev/null
+++ b/test-suite/output/InvalidDisjunctiveIntro.v
@@ -0,0 +1,18 @@
+Theorem test (A:Prop) : A \/ A -> A.
+  Fail intros H; destruct H as H.
+  (* Cannot coerce to a disjunctive/conjunctive pattern. *)
+  Fail intro H; destruct H as H.
+  (* Disjunctive/conjunctive introduction pattern expected. *)
+  Fail let H := fresh in intro H; destruct H as H.
+  (* Cannot coerce to a disjunctive/conjunctive pattern. *)
+  Fail let H := fresh in intros H; destruct H as H.
+  (* Cannot coerce to a disjunctive/conjunctive pattern. *)
+  Fail let H := idtac in intros H; destruct H as H.
+  (* Ltac variable H is bound to <tactic closure> which cannot be
+coerced to an introduction pattern. *)
+  Fail let H := idtac in intros H; destruct H as H'.
+  (* Disjunctive/conjunctive introduction pattern expected. *)
+  Fail let H' := idtac in intros H; destruct H as H'.
+(* Ltac variable H' is bound to <tactic closure> which cannot
+be coerced to an introduction pattern. *)
+Abort.