From bb9d135fce0bc8e12a8dc66a3565b7b84feb1a7c Mon Sep 17 00:00:00 2001
From: Jacques-Henri Jourdan <jjourdan@mpi-sws.org>
Date: Mon, 6 Mar 2017 14:53:04 +0100
Subject: [PATCH] Tweak.

---
 theories/typing/unsafe/rwlock/rwlock.v | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

diff --git a/theories/typing/unsafe/rwlock/rwlock.v b/theories/typing/unsafe/rwlock/rwlock.v
index 17772145..38985be1 100644
--- a/theories/typing/unsafe/rwlock/rwlock.v
+++ b/theories/typing/unsafe/rwlock/rwlock.v
@@ -48,8 +48,9 @@ Section rwlock_inv.
 
   Global Instance rwlock_inv_type_ne n tid l γ α :
     Proper (type_dist2 n ==> dist n) (rwlock_inv tid l γ α).
-  Proof. 
-    solve_proper_core ltac:(fun _ => exact: type_dist2_S || f_type_equiv || f_contractive || f_equiv).
+  Proof.
+    solve_proper_core
+      ltac:(fun _ => exact: type_dist2_S || f_type_equiv || f_contractive || f_equiv).
   Qed.
 
   Global Instance rwlock_inv_ne tid l γ α : NonExpansive (rwlock_inv tid l γ α).
-- 
GitLab