From 5cca350dfd50b75f0f4e6d3b2d3269715cf5b8c4 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Fri, 30 Oct 2015 19:10:50 +0100
Subject: [PATCH] add a helpful comment
---
iris_ht_rules.v | 2 ++
1 file changed, 2 insertions(+)
diff --git a/iris_ht_rules.v b/iris_ht_rules.v
index 80dc1d64c..8a0c03049 100644
--- a/iris_ht_rules.v
+++ b/iris_ht_rules.v
@@ -114,6 +114,8 @@ Module Type IRIS_HT_RULES (RL : VIRA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP:
Proof.
intros w n He. destruct HFill as (HFval & HFstep & HFfstep).
revert e w He; induction n using wf_nat_ind; intros; rename H into IH.
+ (* We need to actually decide whether e is a value, to establish safety in the case that
+ it is not. *)
destruct (is_value_dec e) as [HVal | HNVal]; [clear IH |].
- eapply (wpValue _ HVal) in He. exact:He.
- rewrite ->unfold_wp in He; rewrite unfold_wp. split; intros.
--
GitLab