test-suite/bugs/closed/bug_4580.v


1
2
3
4
5
6
7

Require Import Program.

Class Foo (A : Type) := foo : A.

Unset Refine Instance Mode.
Program Instance f1 : Foo nat := S _.
Next Obligation. exact 0. Defined.