Commit f5d03e25 authored by Ralf Jung's avatar Ralf Jung

be more explicit about quantification order

parent 032f365f
Pipeline #15301 failed with stage
in 0 seconds
......@@ -81,7 +81,7 @@ Proof.
Qed.
Section gen_heap.
Context `{Countable L, !gen_heapG L V Σ}.
Context {L V} `{Countable L, !gen_heapG L V Σ}.
Implicit Types P Q : iProp Σ.
Implicit Types Φ : V iProp Σ.
Implicit Types σ : gmap L V.
......
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