summaryrefslogtreecommitdiff
path: root/test-suite/bugs/closed/3265.v
blob: 269c7b741e364835b5adaf256689abe78710b4be (plain)
1
2
3
4
5
6
Require Import Setoid.
Hint Extern 0 => apply reflexivity : typeclass_instances.
Goal forall (B : Type) (P : B -> Prop), exists y : B, P y.
  intros.
  try reflexivity. (* Anomaly: Uncaught exception Not_found. Please report. *)
Abort.