Commit 2084cf74 authored by Dan Frumin's avatar Dan Frumin

Fix the counter example

parent b8326b06
......@@ -496,7 +496,7 @@ Theorem counter_ctx_refinement :
Proof.
set (Σ := #[invΣ ; gen_heapΣ loc val ; authΣ cfgUR ]).
set (HG := HeapPreIG Σ _ _).
eapply (binary_soundness Σ _).
eapply (logrel_ctxequiv Σ _).
(* TODO: how to get rid of this bullshit with closed conditions? *)
rewrite /FG_counter /CG_counter; try solve_closed.
rewrite /FG_counter /CG_counter; try solve_closed.
......
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