diff --git a/opam b/opam
index 85f03ee787f386463f4eb6dc560d7440065bd8cd..6acce1cd7d786c70f27136a3b0965c67c2c33ae6 100644
--- a/opam
+++ b/opam
@@ -12,5 +12,5 @@ remove: ["rm" "-rf" "%{lib}%/coq/user-contrib/iris"]
 depends: [
   "coq" { >= "8.6.1" & < "8.8~" }
   "coq-mathcomp-ssreflect" { (>= "1.6.1" & < "1.7~") | (= "dev") }
-  "coq-stdpp" { (= "dev.2017-11-18.0") | (= "dev") }
+  "coq-stdpp" { (= "dev.2017-11-20.0") | (= "dev") }
 ]
diff --git a/theories/algebra/ofe.v b/theories/algebra/ofe.v
index b51402803548af145d104f6a582edbf799f359f6..9cf97615e6ec2735d6c76bbf6c6b7a340ec58a75 100644
--- a/theories/algebra/ofe.v
+++ b/theories/algebra/ofe.v
@@ -1061,6 +1061,7 @@ Inductive later (A : Type) : Type := Next { later_car : A }.
 Add Printing Constructor later.
 Arguments Next {_} _.
 Arguments later_car {_} _.
+Instance: Params (@Next) 1.
 
 Section later.
   Context {A : ofeT}.
diff --git a/theories/algebra/sts.v b/theories/algebra/sts.v
index c49f186fc0db0d634dc7058db8c0765f56587cfc..66e4726e9c67e57f4b690e5930614bac087009c9 100644
--- a/theories/algebra/sts.v
+++ b/theories/algebra/sts.v
@@ -79,7 +79,7 @@ Qed.
 Global Instance up_set_preserving : Proper ((⊆) ==> flip (⊆) ==> (⊆)) up_set.
 Proof.
   intros S1 S2 HS T1 T2 HT. rewrite /up_set.
-  f_equiv=> // s1 s2 Hs. by apply up_preserving.
+  f_equiv=> // s1 s2. by apply up_preserving.
 Qed.
 Global Instance up_set_proper : Proper ((≡) ==> (≡) ==> (≡)) up_set.
 Proof.
diff --git a/theories/base_logic/lib/saved_prop.v b/theories/base_logic/lib/saved_prop.v
index b1d1c462a29a1843ff5af67d462f4914c159e15d..e91c5670edf346336cc2e6cd9125420642d0056b 100644
--- a/theories/base_logic/lib/saved_prop.v
+++ b/theories/base_logic/lib/saved_prop.v
@@ -21,7 +21,7 @@ Definition saved_anything_own `{savedAnythingG Σ F}
     (γ : gname) (x : F (iProp Σ)) : iProp Σ :=
   own γ (to_agree $ (cFunctor_map F (iProp_fold, iProp_unfold) x)).
 Typeclasses Opaque saved_anything_own.
-Instance: Params (@saved_anything_own) 3.
+Instance: Params (@saved_anything_own) 4.
 
 Section saved_anything.
   Context `{savedAnythingG Σ F}.
diff --git a/theories/base_logic/lib/wsat.v b/theories/base_logic/lib/wsat.v
index bfa226e3c8013cec1606c5ecd3d006fa9b23c923..a26f4f6ae6395fd36dfc415e01f14410ffd7d46c 100644
--- a/theories/base_logic/lib/wsat.v
+++ b/theories/base_logic/lib/wsat.v
@@ -23,6 +23,7 @@ Definition ownI `{invG Σ} (i : positive) (P : iProp Σ) : iProp Σ :=
   own invariant_name (â—¯ {[ i := invariant_unfold P ]}).
 Arguments ownI {_ _} _ _%I.
 Typeclasses Opaque ownI.
+Instance: Params (@invariant_unfold) 1.
 Instance: Params (@ownI) 3.
 
 Definition ownE `{invG Σ} (E : coPset) : iProp Σ :=