From 5af1b29ad81a97f73c819557906e0a6f71777962 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Wed, 6 Sep 2017 16:07:51 +0200
Subject: [PATCH] Bump coq-stdpp.

---
 opam.pins                        | 2 +-
 theories/proofmode/coq_tactics.v | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

diff --git a/opam.pins b/opam.pins
index b685c00b8..d5fd7ce49 100644
--- a/opam.pins
+++ b/opam.pins
@@ -1 +1 @@
-coq-stdpp https://gitlab.mpi-sws.org/robbertkrebbers/coq-stdpp fa6ff9d18aefb29e839e815aa170262d330bd108
+coq-stdpp https://gitlab.mpi-sws.org/robbertkrebbers/coq-stdpp 2d27f42b9c4d9e5c0810122779a93873050fb756
diff --git a/theories/proofmode/coq_tactics.v b/theories/proofmode/coq_tactics.v
index 821092226..775d56558 100644
--- a/theories/proofmode/coq_tactics.v
+++ b/theories/proofmode/coq_tactics.v
@@ -493,7 +493,7 @@ Qed.
 
 (** * Implication and wand *)
 Lemma tac_impl_intro Δ Δ' i P Q :
-  (if env_spatial_is_nil Δ then Unit else PersistentP P) →
+  (if env_spatial_is_nil Δ then TCTrue else PersistentP P) →
   envs_app false (Esnoc Enil i P) Δ = Some Δ' →
   (Δ' ⊢ Q) → Δ ⊢ P → Q.
 Proof.
-- 
GitLab