1 files changed, 24 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/4782.v b/test-suite/bugs/closed/4782.v
new file mode 100644
index 00000000..dbd71035
--- /dev/null
+++ b/test-suite/bugs/closed/4782.v
@@ -0,0 +1,24 @@
+(* About typing of with bindings *)
+
+Record r : Type := mk_r { type : Type; cond : type -> Prop }.
+
+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).
+