4580.v « closed « bugs « test-suite - debian-coq - Debian packaging for Coq

summary refs log tree commit diff

path: root/test-suite/bugs/closed/4580.v

blob: 4ffd5f0f4be76ed7411cb925d4f4b55507d8c7b0 (plain)

Require Import Program.

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

Unset Refine Instance Mode.
Program Instance f1 : Foo nat := S _.