Commit 03c3a419 authored by Dan Frumin's avatar Dan Frumin

Make the basic operations opaque

parent 12968f8d
......@@ -230,6 +230,9 @@ Section a_wp_run.
Qed.
End a_wp_run.
(* Make sure that we only use the provided rules and don't break the abstraction *)
Opaque a_ret a_bind (* a_run *) a_atomic a_atomic_env a_par.
(* Definition locking_heapΣ : gFunctors := *)
(* #[heapΣ; GFunctor (auth.authR locking_heapUR)]. *)
......
......@@ -296,4 +296,8 @@ Section proofs.
iIntros (v) "Hi". iModIntro. awp_seq.
by iApply ("IH" with "Hi").
Qed.
End proofs.
(* Make sure that we only use the provided rules and don't break the abstraction *)
Opaque a_alloc a_store a_load a_un_op a_bin_op a_seq a_seq_bind a_if a_while.
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