Commit 1bd7e954 authored by Gaurav Parthasarathy's avatar Gaurav Parthasarathy

fixed hint

parent 3f2a1f72
Pipeline #17853 canceled with stage
......@@ -242,7 +242,7 @@ Section rdcss.
pau P Q γ_n l_m m1 n1 n2 is_gc_loc l_m
end)%I.
Local Hint Extern 0 (environments.envs_entails _ (rdcss_inv _ _ _ _)) => unfold rdcss_inv.
Local Hint Extern 0 (environments.envs_entails _ (rdcss_inv _ _)) => unfold rdcss_inv.
Definition is_rdcss (γ_n : gname) (rdcss_data: val) :=
( (l_n : loc), rdcss_data = #l_n inv rdcssN (rdcss_inv γ_n l_n) gc_inv N ## gcN)%I.
......
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