Commit e2c29658 authored by Dan Frumin's avatar Dan Frumin

A small clear up

parent 58f5ee24
...@@ -2,7 +2,6 @@ From iris_logrel.F_mu Require Export fundamental. ...@@ -2,7 +2,6 @@ From iris_logrel.F_mu Require Export fundamental.
From iris.proofmode Require Import tactics. From iris.proofmode Require Import tactics.
From iris.program_logic Require Import adequacy. From iris.program_logic Require Import adequacy.
Theorem soundness Σ `{invPreG Σ} e τ e' thp σ σ' : Theorem soundness Σ `{invPreG Σ} e τ e' thp σ σ' :
( `{irisG lang Σ}, log_typed [] e τ) ( `{irisG lang Σ}, log_typed [] e τ)
rtc step ([e], σ) (thp, σ') e' thp rtc step ([e], σ) (thp, σ') e' thp
......
...@@ -59,7 +59,6 @@ Lemma binary_soundness Σ `{heapPreG Σ, authG Σ cfgUR} ...@@ -59,7 +59,6 @@ Lemma binary_soundness Σ `{heapPreG Σ, authG Σ cfgUR}
( `{cfgSG Σ} `{!heapG Σ}, Γ e log e' : τ) ( `{cfgSG Σ} `{!heapG Σ}, Γ e log e' : τ)
Γ e ctx e' : τ. Γ e ctx e' : τ.
Proof. Proof.
intros He He' Hlog K thp σ v ?. eapply (basic_soundness Σ)=> ?. intros He He' Hlog K thp σ v ?. eapply (basic_soundness Σ)=> ??.
intros ?.
eapply (bin_log_related_under_typed_ctx _ _ _ _ []); eauto. eapply (bin_log_related_under_typed_ctx _ _ _ _ []); eauto.
Qed. Qed.
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment