From 8c6c9404e69ce986b43802438461a5fcb7a744af Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Fri, 24 Nov 2017 15:25:53 +0100
Subject: [PATCH] pure_exec_ctx is a too general instance

---
 theories/program_logic/ectx_language.v | 6 ++++++
 theories/program_logic/language.v      | 3 ++-
 2 files changed, 8 insertions(+), 1 deletion(-)

diff --git a/theories/program_logic/ectx_language.v b/theories/program_logic/ectx_language.v
index 34a366329..3c20309d3 100644
--- a/theories/program_logic/ectx_language.v
+++ b/theories/program_logic/ectx_language.v
@@ -205,6 +205,12 @@ Section ectx_language.
       eexists e2', σ2, efs. by apply head_prim_step.
     - intros σ1 e2' σ2 efs ? ?%head_reducible_prim_step; eauto.
   Qed.
+
+  Global Instance pure_exec_fill K e1 e2 φ :
+    PureExec φ e1 e2 →
+    PureExec φ (fill K e1) (fill K e2).
+  Proof. apply: pure_exec_ctx. Qed.
+
 End ectx_language.
 
 Arguments ectx_lang : clear implicits.
diff --git a/theories/program_logic/language.v b/theories/program_logic/language.v
index b9d10beb8..a3704c702 100644
--- a/theories/program_logic/language.v
+++ b/theories/program_logic/language.v
@@ -140,7 +140,8 @@ Section language.
     PureExec P e1 e2.
   Proof. intros HPE. split; intros; eapply HPE; eauto. Qed.
 
-  Global Instance pure_exec_ctx K `{LanguageCtx Λ K} e1 e2 φ :
+  (* We do not make this an instance because it is awfully general. *)
+  Lemma pure_exec_ctx K `{LanguageCtx Λ K} e1 e2 φ :
     PureExec φ e1 e2 →
     PureExec φ (K e1) (K e2).
   Proof.
-- 
GitLab