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

forward a FIXME to the Coq bugtacker

parent 4ae55518
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
Showing
with 1 addition and 1 deletion
barrier/lifting.v
+ 1
− 1
View file @ eec1486d
...@@ -21,8 +21,8 @@ Lemma wp_lift_step E1 E2 (φ : expr → state → Prop) Q e1 σ1 : ...@@ -21,8 +21,8 @@ Lemma wp_lift_step E1 E2 (φ : expr → state → Prop) Q e1 σ1 :
pvs E1 E2 (wp (Σ:=Σ) E2 e2 Q)) pvs E1 E2 (wp (Σ:=Σ) E2 e2 Q))
⊑ wp (Σ:=Σ) E2 e1 Q. ⊑ wp (Σ:=Σ) E2 e1 Q.
Proof. Proof.
(* RJ FIXME WTF the bound names of wp_lift_step *changed*?!?? *)
intros ? He Hsafe Hstep. intros ? He Hsafe Hstep.
(* RJ: working around https://coq.inria.fr/bugs/show_bug.cgi?id=4536 *)
etransitivity; last eapply wp_lift_step with (σ2 := σ1) etransitivity; last eapply wp_lift_step with (σ2 := σ1)
(φ0 := λ e' σ' ef, ef = None ∧ φ e' σ'); last first. (φ0 := λ e' σ' ef, ef = None ∧ φ e' σ'); last first.
- intros e2 σ2 ef Hstep'%prim_ectx_step; last done. - intros e2 σ2 ef Hstep'%prim_ectx_step; last done.
......
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