Skip to content
Snippets Groups Projects
Commit 5180d1cd authored by Ralf Jung's avatar Ralf Jung
Browse files

fix build

parent 2891ccae
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
theories/program_logic/ownp.v
+ 3
− 1
View file @ 5180d1cd
...@@ -219,7 +219,9 @@ Section ectx_lifting. ...@@ -219,7 +219,9 @@ Section ectx_lifting.
(∀ σ1 e2' σ2 efs', head_step e1 σ1 e2' σ2 efs' → σ1 = σ2 ∧ e2 = e2' ∧ efs = efs') → (∀ σ1 e2' σ2 efs', head_step e1 σ1 e2' σ2 efs' → σ1 = σ2 ∧ e2 = e2' ∧ efs = efs') →
▷ (WP e2 @ E {{ Φ }} ∗ [∗ list] ef ∈ efs, WP ef {{ _, True }}) ▷ (WP e2 @ E {{ Φ }} ∗ [∗ list] ef ∈ efs, WP ef {{ _, True }})
⊢ WP e1 @ E {{ Φ }}. ⊢ WP e1 @ E {{ Φ }}.
Proof using Hinh. eauto using wp_lift_pure_det_step. Qed. Proof using Hinh.
intros. rewrite -[(WP e1 @ _ {{ _ }})%I]wp_lift_pure_det_step; eauto.
Qed.
Lemma ownP_lift_pure_det_head_step_no_fork {E Φ} e1 e2 : Lemma ownP_lift_pure_det_head_step_no_fork {E Φ} e1 e2 :
to_val e1 = None → to_val e1 = None →
......
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