test-suite/bugs/closed/gh6384.v


1
2
3
4
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.