5 files changed, 45 insertions, 1 deletions
diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml
index e0d7eca5f..249ac93fc 100644
--- a/plugins/ltac/tacinterp.ml
+++ b/plugins/ltac/tacinterp.ml
@@ -890,7 +890,7 @@ let interp_intro_pattern_naming_option ist env sigma = function
 let interp_or_and_intro_pattern_option ist env sigma = function
   | None -> sigma, None
   | Some (ArgVar (loc,id)) ->
-      (match coerce_to_intro_pattern env sigma (Id.Map.find id ist.lfun) with
+      (match interp_intro_pattern_var loc ist env sigma id with
       | IntroAction (IntroOrAndPattern l) -> sigma, Some (loc,l)
       | _ ->
         user_err ?loc (str "Cannot coerce to a disjunctive/conjunctive pattern."))
diff --git a/test-suite/bugs/closed/gh6384.v b/test-suite/bugs/closed/gh6384.v
new file mode 100644
index 000000000..cec84642f
--- /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 000000000..3bbb664f4
--- /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 000000000..25a306b45
--- /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 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.