From db002583b18c8742c0cd8e1a12305166b6b791ce Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Thu, 12 Nov 2015 12:05:00 +0100
Subject: Fixed test-suite file for bug #3998.

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

diff --git a/test-suite/bugs/closed/3998.v b/test-suite/bugs/closed/3998.v
new file mode 100644
index 0000000000..ced13839dd
--- /dev/null
+++ b/test-suite/bugs/closed/3998.v
@@ -0,0 +1,24 @@
+Class FieldType (F : Set) := mkFieldType { fldTy: F -> Set }.
+Hint Mode FieldType + : typeclass_instances. (* The F parameter is an input *)
+
+Inductive I1 := C.
+Inductive I2 := .
+
+Instance I1FieldType : FieldType I1 := { fldTy := I1_rect _ bool }.
+Instance I2FieldType : FieldType I2 := { fldTy := I2_rect _ }.
+
+Definition RecordOf F (FT: FieldType F) := forall f:F, fldTy f.
+
+Class MapOps (M K : Set) := {
+  tgtTy: K -> Set;
+  update: M -> forall k:K, tgtTy k -> M
+}.
+
+Instance RecordMapOps F (FT: FieldType F) : MapOps (RecordOf F FT) F :=
+{ tgtTy := fldTy; update := fun r (f: F) (x: fldTy f) z => r z }.
+
+Axiom ex : RecordOf _ I1FieldType.
+
+Definition works := (fun ex' => update ex' C true) (update ex C false).
+Set Typeclasses Debug.
+Definition doesnt := update (update ex C false) C true.
\ No newline at end of file
-- 
cgit v1.2.3