From 2b04cb3b71eff4b58dcf246637c002dd64ad1b37 Mon Sep 17 00:00:00 2001
From: Dan Frumin <dfrumin@cs.ru.nl>
Date: Mon, 2 Mar 2020 13:19:58 +0100
Subject: [PATCH] Generalize `refines_typed`.
---
theories/typing/fundamental.v | 6 +++---
1 file changed, 3 insertions(+), 3 deletions(-)
diff --git a/theories/typing/fundamental.v b/theories/typing/fundamental.v
index 0ef44e0..f583c71 100644
--- a/theories/typing/fundamental.v
+++ b/theories/typing/fundamental.v
@@ -503,12 +503,12 @@ Section fundamental.
- by iApply (bin_log_related_CmpXchg with "[] []").
Qed.
- Theorem refines_typed e Ï„ :
+ Theorem refines_typed τ Δ e :
∅ ⊢ₜ e : τ →
- REL e << e : (interp Ï„ []).
+ REL e << e : (interp τ Δ ).
Proof.
move=> /binary_fundamental Hty.
- iPoseProof (Hty [] with "[]") as "H".
+ iPoseProof (Hty Δ with "[]") as "H".
{ rewrite fmap_empty. iApply env_ltyped2_empty. }
by rewrite !fmap_empty !subst_map_empty.
Qed.
--
GitLab