aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/bugs/closed/4412.v
blob: 4b2aae0c7ba95e736f44cd5836dd7bdd662b0e15 (plain)
1
2
3
4
Require Import Coq.Bool.Bool Coq.Setoids.Setoid.
Goal forall (P : forall b : bool, b = true -> Type) (x y : bool) (H : andb x y = true) (H' : P _ H), True.
  intros.
  Fail rewrite Bool.andb_true_iff in H.