test-suite/output/bug12442.v


1
2
3
4
5
6
7
8
9
10

Parameter A B : Prop.
Axiom P : inhabited (A -> B).

Goal A -> True.
Proof.
  Fail intros ?%P ?.
  Fail intros []%P.
  intro a.
  Fail apply P in a as [].
Abort.