test-suite/bugs/closed/bug_4580.v


1
2
3
4
5
6

Require Import Program.

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

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