From bc2298c3cefc35f3ef426a102da4b93eb319b4cb Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Wed, 24 Feb 2016 10:21:23 +0100
Subject: [PATCH] barrier: fix compilation

---
 barrier/barrier.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/barrier/barrier.v b/barrier/barrier.v
index b9504e560..8de4a99de 100644
--- a/barrier/barrier.v
+++ b/barrier/barrier.v
@@ -364,7 +364,7 @@ Section proof.
       rewrite [(_ ★ heap_ctx _)%I]comm -!assoc.
       rewrite const_equiv // left_id -pvs_frame_l. apply sep_mono_r.
       rewrite comm -pvs_frame_l. apply sep_mono_r.
-      apply sts_ownS_weaken; eauto using sts.up_subseteq with sts. }
+      apply sts_own_weaken; eauto using sts.up_subseteq with sts. }
     (* a High state: the comparison succeeds, and we perform a transition and
        return to the client *)
     rewrite [(_ ★ □ (_ → _ ))%I]sep_elim_l.
-- 
GitLab