Catch errors while coercing 'and' intro patterns

Fixes GH#6384 and GH#6385.

1 files changed, 18 insertions, 0 deletions

diff --git a/test-suite/output/InvalidDisjunctiveIntro.v b/test-suite/output/InvalidDisjunctiveIntro.v
new file mode 100644
index 000000000..4febdf034
--- /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.