From ccc7a5df705fbcfbabae52b47c0eadfba0a7a04b Mon Sep 17 00:00:00 2001 From: Ralf Jung <jung@mpi-sws.org> Date: Tue, 23 Feb 2016 10:53:07 +0100 Subject: [PATCH] fix the build --- barrier/barrier.v | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/barrier/barrier.v b/barrier/barrier.v index c36779a22..a08052869 100644 --- a/barrier/barrier.v +++ b/barrier/barrier.v @@ -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 Σ). -- GitLab