From b57aa587446d1b096643950cc0ed3e975a210c2e Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Mon, 7 Oct 2019 12:03:16 +0200
Subject: [PATCH] Use `TCEq` so that TC search can establish non-valueness.

---
 theories/program_logic/weakestpre.v | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/theories/program_logic/weakestpre.v b/theories/program_logic/weakestpre.v
index 6d3a96670..3752b6a0e 100644
--- a/theories/program_logic/weakestpre.v
+++ b/theories/program_logic/weakestpre.v
@@ -79,8 +79,8 @@ Global Instance wp_proper s E e :
 Proof.
   by intros Φ Φ' ?; apply equiv_dist=>n; apply wp_ne=>v; apply equiv_dist.
 Qed.
-Lemma wp_contractive s E e n :
-  to_val e = None →
+Global Instance wp_contractive s E e n :
+  TCEq (to_val e) None →
   Proper (pointwise_relation _ (dist_later n) ==> dist n) (wp (PROP:=iProp Σ) s E e).
 Proof.
   intros He Φ Ψ HΦ. rewrite !wp_unfold /wp_pre He.
-- 
GitLab