From 53f6857fafb25601d072d2b948b1b92f62834719 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Wed, 4 Jan 2017 18:03:23 +0100
Subject: [PATCH] =?UTF-8?q?Tweak=20lib/sts=20so=20not=20all=20lemmas=20are?=
 =?UTF-8?q?=20parametrized=20by=20=CF=86.?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 theories/base_logic/lib/sts.v | 13 +++++++------
 1 file changed, 7 insertions(+), 6 deletions(-)

diff --git a/theories/base_logic/lib/sts.v b/theories/base_logic/lib/sts.v
index 9fd943628..e66b620f8 100644
--- a/theories/base_logic/lib/sts.v
+++ b/theories/base_logic/lib/sts.v
@@ -58,7 +58,8 @@ Instance: Params (@sts_own) 5.
 Instance: Params (@sts_ctx) 6.
 
 Section sts.
-  Context `{invG Î£, stsG Î£ sts} (Ï† : sts.state sts â†’ iProp Î£).
+  Context `{invG Î£, stsG Î£ sts}.
+  Implicit Types Ï† : sts.state sts â†’ iProp Î£.
   Implicit Types N : namespace.
   Implicit Types P Q R : iProp Î£.
   Implicit Types Î³ : gname.
@@ -82,7 +83,7 @@ Section sts.
     sts_ownS Î³ (S1 âˆ© S2) (T1 âˆª T2) âŠ£âŠ¢ (sts_ownS Î³ S1 T1 âˆ— sts_ownS Î³ S2 T2).
   Proof. intros. by rewrite /sts_ownS -own_op sts_op_frag. Qed.
 
-  Lemma sts_alloc E N s :
+  Lemma sts_alloc Ï† E N s :
     â–· Ï† s ={E}=âˆ— âˆƒ Î³, sts_ctx Î³ N Ï† âˆ§ sts_own Î³ s (âŠ¤ âˆ– sts.tok s).
   Proof.
     iIntros "HÏ†". rewrite /sts_ctx /sts_own.
@@ -93,7 +94,7 @@ Section sts.
     rewrite /sts_inv. iNext. iExists s. by iFrame.
   Qed.
 
-  Lemma sts_accS E Î³ S T :
+  Lemma sts_accS Ï† E Î³ S T :
     â–· sts_inv Î³ Ï† âˆ— sts_ownS Î³ S T ={E}=âˆ— âˆƒ s,
       âŒœs âˆˆ SâŒ âˆ— â–· Ï† s âˆ— âˆ€ s' T',
       âŒœsts.steps (s, T) (s', T')âŒ âˆ— â–· Ï† s' ={E}=âˆ— â–· sts_inv Î³ Ï† âˆ— sts_own Î³ s' T'.
@@ -111,13 +112,13 @@ Section sts.
     iModIntro. iNext. iExists s'; by iFrame.
   Qed.
 
-  Lemma sts_acc E Î³ s0 T :
+  Lemma sts_acc Ï† E Î³ s0 T :
     â–· sts_inv Î³ Ï† âˆ— sts_own Î³ s0 T ={E}=âˆ— âˆƒ s,
       âŒœsts.frame_steps T s0 sâŒ âˆ— â–· Ï† s âˆ— âˆ€ s' T',
       âŒœsts.steps (s, T) (s', T')âŒ âˆ— â–· Ï† s' ={E}=âˆ— â–· sts_inv Î³ Ï† âˆ— sts_own Î³ s' T'.
   Proof. by apply sts_accS. Qed.
 
-  Lemma sts_openS E N Î³ S T :
+  Lemma sts_openS Ï† E N Î³ S T :
     â†‘N âŠ† E â†’
     sts_ctx Î³ N Ï† âˆ— sts_ownS Î³ S T ={E,Eâˆ–â†‘N}=âˆ— âˆƒ s,
       âŒœs âˆˆ SâŒ âˆ— â–· Ï† s âˆ— âˆ€ s' T',
@@ -135,7 +136,7 @@ Section sts.
     iMod ("HclSts" $! s' T' with "H") as "(Hinv & ?)". by iMod ("Hclose" with "Hinv").
   Qed.
 
-  Lemma sts_open E N Î³ s0 T :
+  Lemma sts_open Ï† E N Î³ s0 T :
     â†‘N âŠ† E â†’
     sts_ctx Î³ N Ï† âˆ— sts_own Î³ s0 T ={E,Eâˆ–â†‘N}=âˆ— âˆƒ s,
       âŒœsts.frame_steps T s0 sâŒ âˆ— â–· Ï† s âˆ— âˆ€ s' T',
-- 
GitLab