From e8f25c81fe22de359cfeafbb1f7e464d2aa2b46c Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Thu, 24 Jan 2019 22:48:30 +0100
Subject: [PATCH] a note on TC resolution

---
 theories/heap_lang/proofmode.v | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/theories/heap_lang/proofmode.v b/theories/heap_lang/proofmode.v
index 93359a4b3..92851e213 100644
--- a/theories/heap_lang/proofmode.v
+++ b/theories/heap_lang/proofmode.v
@@ -357,7 +357,8 @@ End heap.
 
 (** Evaluate [lem] to a hypothesis [H] that can be applied, and then run
 [wp_bind K; tac H] for every possible evaluation context.  [tac] can do
-[iApplyHyp H] to actually apply the hypothesis. *)
+[iApplyHyp H] to actually apply the hypothesis.  TC resolution of [lem] premises
+happens *after* [tac H] got executed. *)
 Tactic Notation "wp_apply_core" open_constr(lem) tactic(tac) :=
   wp_pures;
   iPoseProofCore lem as false true (fun H =>
-- 
GitLab