diff --git a/opam b/opam
index 8d3353de4e5e180878395f54af5e15578d2ade30..1b429b5761ecc209c7bb0d147ede84e79dc71d9c 100644
--- a/opam
+++ b/opam
@@ -11,5 +11,5 @@ install: [make "install"]
 remove: ["rm" "-rf" "%{lib}%/coq/user-contrib/iris"]
 depends: [
   "coq" { (>= "8.7.1" & < "8.9~") | (= "dev") }
-  "coq-stdpp" { (= "dev.2018-06-20.0.b2ca5d48") | (= "dev") }
+  "coq-stdpp" { (= "dev.2018-06-25.1.0eb9a89b") | (= "dev") }
 ]
diff --git a/tests/algebra.v b/tests/algebra.v
index 8505ef20131e4fe84700ebc0b9b36fbc23cefd9b..0ec719eac82be93cfeecc39573369c566b27bfd5 100644
--- a/tests/algebra.v
+++ b/tests/algebra.v
@@ -8,3 +8,19 @@ Section tests.
   Solve Obligations with solve_proper.
 
 End tests.
+
+(** Check that [@Reflexive Prop ?r] picks the instance setoid_rewrite needs.
+    Really, we want to set [Hint Mode Reflexive] in a way that this fails, but
+    we cannot [1].  So at least we try to make sure the first solution found
+    is the right one, to not pay performance in the success case [2].
+
+    [1] https://github.com/coq/coq/issues/7916
+    [2] https://gitlab.mpi-sws.org/robbertkrebbers/coq-stdpp/merge_requests/38
+*)
+Lemma test_setoid_rewrite :
+  exists R, @Reflexive Prop R /\ R = iff.
+Proof.
+  eexists. split.
+  - apply _.
+  - reflexivity.
+Qed.