From 69ae6e7d1c591b173cb64578b194529411b90cea Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Wed, 11 Feb 2015 00:42:31 +0100
Subject: Adding test for bug #3900.

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

diff --git a/test-suite/bugs/closed/3900.v b/test-suite/bugs/closed/3900.v
new file mode 100644
index 0000000000..6be2161c2f
--- /dev/null
+++ b/test-suite/bugs/closed/3900.v
@@ -0,0 +1,13 @@
+Global Set Primitive Projections.
+Set Implicit Arguments.
+Record sigT {A} (P : A -> Type) := existT { projT1 : A ; projT2 : P projT1 }.
+Record PreCategory := { object :> Type ; morphism : object -> object -> Type }.
+Variable A : PreCategory.
+Variable Pobj : A -> Type.
+Local Notation obj := (sigT Pobj).
+Variable Pmor : forall s d : obj, morphism A (projT1 s) (projT1 d) -> Type.
+Class Foo (x : Type) := { _ : forall y, y }.
+Local Instance ishset_pmor {s d m} : Foo (Pmor s d m).
+Proof.
+SearchAbout ((forall _ _, _) -> Foo _).
+Abort.
-- 
cgit v1.2.3