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

remove trailing space

parent 5fbf777b
No related branches found
No related tags found
No related merge requests found
......@@ -171,7 +171,7 @@ Section gen_heap.
Proof. rewrite pointsto_unseal. apply ghost_map_elem_combine. Qed.
Global Instance pointsto_combine_as l dq1 dq2 v1 v2 :
CombineSepAs (l {dq1} v1) (l {dq2} v2) (l {dq1 dq2} v1) | 60.
CombineSepAs (l {dq1} v1) (l {dq2} v2) (l {dq1 dq2} v1) | 60.
(* higher cost than the Fractional instance, which kicks in for #qs *)
Proof.
rewrite /CombineSepAs. iIntros "[H1 H2]".
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment