From 924d2833644735a9fa8289ffaa9bac9fbc43982c Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Fri, 19 Feb 2016 14:27:31 +0100
Subject: Fixing bug #4580: [Set Refine Instance Mode] also used for Program
 Instance.

---
 test-suite/bugs/closed/4580.v | 6 ++++++
 1 file changed, 6 insertions(+)
 create mode 100644 test-suite/bugs/closed/4580.v

(limited to 'test-suite')

diff --git a/test-suite/bugs/closed/4580.v b/test-suite/bugs/closed/4580.v
new file mode 100644
index 0000000000..4ffd5f0f4b
--- /dev/null
+++ b/test-suite/bugs/closed/4580.v
@@ -0,0 +1,6 @@
+Require Import Program.
+
+Class Foo (A : Type) := foo : A.
+
+Unset Refine Instance Mode.
+Program Instance f1 : Foo nat := S _.
-- 
cgit v1.2.3