1 files changed, 15 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/4782.v b/test-suite/bugs/closed/4782.v
index ed4443786..dbd71035d 100644
--- a/test-suite/bugs/closed/4782.v
+++ b/test-suite/bugs/closed/4782.v
@@ -7,3 +7,18 @@ Inductive p : Prop := consp : forall (e : r) (x : type e), cond e x -> p.
 Goal p.
 Fail apply consp with (fun _ : bool => mk_r unit (fun x => True)) nil.
  
+(* A simplification of an example from coquelicot, which was failing
+   at some time after a fix #4782 was committed. *)
+
+Record T := { dom : Type }.
+Definition pairT A B := {| dom := (dom A * dom B)%type |}.
+Class C (A:Type).
+Parameter B:T.
+Instance c (A:T) : C (dom A).
+Instance cn : C (dom B).
+Parameter F : forall A:T, C (dom A) -> forall x:dom A, x=x -> A = A.
+Set Typeclasses Debug.
+Goal forall (A:T) (x:dom A), pairT A A = pairT A A.
+intros.
+apply (F _ _)  with (x,x).
+