1 files changed, 26 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/3911.v b/test-suite/bugs/closed/3911.v
new file mode 100644
index 00000000..b289eafb
--- /dev/null
+++ b/test-suite/bugs/closed/3911.v
@@ -0,0 +1,26 @@
+(* Tested against coq ee596bc *)
+ 
+Set Nonrecursive Elimination Schemes.
+Set Primitive Projections.
+Set Universe Polymorphism.
+ 
+Record setoid := { base : Type }.
+ 
+Definition catdata (Obj Arr : Type) : Type := nat.
+  (* [nat] can be replaced by any other type, it seems,
+     without changing the error *)
+ 
+Record cat : Type :=
+  {
+    obj : setoid;
+    arr : Type;
+    dta : catdata (base obj) arr
+  }.
+ 
+Definition bcwa (C:cat) (B:setoid) :Type := nat.
+  (* As above, nothing special about [nat] here. *)
+ 
+Record temp {C}{B} (e:bcwa C B) :=
+  { fld : base (obj C) }.
+ 
+Print temp_rect.