aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/bugs/closed/5193.v
blob: cc8739afe67acdf5ad088c7d6cb3ecad25c9c0b8 (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
Class Eqdec A := eqdec : forall a b : A, {a=b}+{a<>b}.

Typeclasses eauto := debug.
Set Typeclasses Debug Verbosity 2.

Inductive Finx(n : nat) : Set :=
| Fx1(i : nat)(e : n = S i)
| FxS(i : nat)(f : Finx i)(e : n = S i).

Context `{Finx_eqdec : forall n, Eqdec (Finx n)}.

Goal {x : Type & Eqdec x}.
  eexists.
  try typeclasses eauto 1 with typeclass_instances.