From 4e11257b1e27007c7239e05ef8e89f5aa5be81a8 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Wed, 17 Feb 2016 12:18:49 +0100
Subject: [PATCH] Shorten sts_ownS_op.

Do not use proper explicitly but let setoids handle it.
---
 program_logic/sts.v | 5 +----
 1 file changed, 1 insertion(+), 4 deletions(-)

diff --git a/program_logic/sts.v b/program_logic/sts.v
index a0807ace1..1a7b45ed1 100644
--- a/program_logic/sts.v
+++ b/program_logic/sts.v
@@ -66,10 +66,7 @@ Section sts.
   Lemma sts_ownS_op γ S1 S2 T1 T2 :
     T1 ∪ T2 ⊆ ∅ → sts.closed S1 T1 → sts.closed S2 T2 →
     sts_ownS γ (S1 ∩ S2) (T1 ∪ T2) ≡ (sts_ownS γ S1 T1 ★ sts_ownS γ S2 T2)%I.
-  Proof.
-    intros HT HS1 HS2. rewrite /sts_ownS -own_op.
-      by apply own_proper, sts_op_frag.
-  Qed.
+  Proof. intros. by rewrite /sts_ownS -own_op sts_op_frag. Qed.
 
   Lemma sts_alloc E N s :
     nclose N ⊆ E →
-- 
GitLab