Commit ccc7a5df authored by Ralf Jung's avatar Ralf Jung

fix the build

parent 35ac5e8e
......@@ -482,8 +482,7 @@ End proof.
Section spec.
Context {Σ : iFunctorG}.
Context `{heapG Σ}.
Context `{stsG heap_lang Σ barrier_proto.sts}.
Context `{savedPropG heap_lang Σ}.
Context `{inGF heap_lang Σ (stsGF sts)} `{inGF heap_lang Σ agreeF}.
Local Notation iProp := (iPropG heap_lang Σ).
......
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