From 7a04946dc451f5d91a1259429bdd1af81c6b9f9f Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Mon, 20 Nov 2017 21:19:42 +0100
Subject: [PATCH] Bump stdpp.

---
 opam                   | 2 +-
 theories/algebra/sts.v | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

diff --git a/opam b/opam
index 85f03ee78..6acce1cd7 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/sts.v b/theories/algebra/sts.v
index c49f186fc..66e4726e9 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.
-- 
GitLab