diff --git a/opam b/opam
index 1804bd0a9e137e82470dee3782d301ea6ffb1deb..96a1b6ce42198be82ba61ded5fd5f1c51aada1aa 100644
--- a/opam
+++ b/opam
@@ -12,5 +12,5 @@ remove: ["rm" "-rf" "%{lib}%/coq/user-contrib/iris"]
 depends: [
   "coq" { (>= "8.6.1" & < "8.8~") | (= "dev") }
   "coq-mathcomp-ssreflect" { (>= "1.6.1" & < "1.7~") | (= "dev") }
-  "coq-stdpp" { (= "dev.2017-11-29.0") | (= "dev") }
+  "coq-stdpp" { (= "dev.2017-11-29.1") | (= "dev") }
 ]
diff --git a/theories/algebra/cmra.v b/theories/algebra/cmra.v
index 91d626f8377227cd50b67d2a66e555ebce6f7594..cd042a56ee6475e1fbf493bb4cb9f398c62336b8 100644
--- a/theories/algebra/cmra.v
+++ b/theories/algebra/cmra.v
@@ -1514,7 +1514,7 @@ Section ofe_fun_cmra.
       { intros x. specialize (Hf12 x).
         destruct (cmra_extend n (f x) (f1 x) (f2 x)) as (y1&y2&?&?&?); eauto.
         exists (y1,y2); eauto. }
-      exists (λ x, gg x.1), (λ x, gg x.2). split_and!=> -?; naive_solver.
+      exists (λ x, (gg x).1), (λ x, (gg x).2). split_and!=> -?; naive_solver.
   Qed.
   Canonical Structure ofe_funR := CmraT (ofe_fun B) ofe_fun_cmra_mixin.