test-suite/bugs/closed/gh6385.v


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