From 0274b81f3eda3608d8cf82e164ffe967d622c471 Mon Sep 17 00:00:00 2001
From: Jacques-Henri Jourdan <jjourdan@mpi-sws.org>
Date: Tue, 8 Nov 2016 20:22:04 +0100
Subject: [PATCH] Tweak.

---
 theories/lifetime.v | 12 ++++++------
 1 file changed, 6 insertions(+), 6 deletions(-)

diff --git a/theories/lifetime.v b/theories/lifetime.v
index 2956516d..bfa9e8d9 100644
--- a/theories/lifetime.v
+++ b/theories/lifetime.v
@@ -47,15 +47,15 @@ Section defs.
   Definition idx_borrow_own (q : Qp) (i : borrow_idx) :=
     own borrow_tok_name (â—¯ {[ i := q ]}).
 
-End defs.
+  Parameter idx_borrow:
+    ∀ `{lifetimeG Σ} (κ : lifetime) (i : borrow_idx) (P : iProp Σ), iProp Σ.
 
-Typeclasses Opaque lft_own lft_dead .
+  Definition borrow (κ : lifetime) (P : iProp Σ) : iProp Σ :=
+    (∃ i, idx_borrow κ i P ∗ idx_borrow_own 1 i)%I.
 
-Parameter idx_borrow:
-  ∀ `{lifetimeG Σ} (κ : lifetime) (i : borrow_idx) (P : iProp Σ), iProp Σ.
+End defs.
 
-Definition borrow `{lifetimeG Σ} (κ : lifetime) (P : iProp Σ) : iProp Σ :=
-  (∃ i, idx_borrow κ i P ∗ idx_borrow_own 1 i)%I.
+Typeclasses Opaque lft_own lft_dead borrow.
 
 (*** Notations  *)
 
-- 
GitLab