From bf5de571597f25f1199a0742bf38507d584dd843 Mon Sep 17 00:00:00 2001
From: Jacques-Henri Jourdan <jacques-henri.jourdan@normalesup.org>
Date: Sun, 11 Dec 2016 12:44:15 +0100
Subject: [PATCH] Remove warning.

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

diff --git a/theories/lifetime/primitive.v b/theories/lifetime/primitive.v
index 4aa81f91..a7c48a0a 100644
--- a/theories/lifetime/primitive.v
+++ b/theories/lifetime/primitive.v
@@ -51,7 +51,7 @@ Proof.
   iIntros "[Hx Hy]".
   iDestruct "Hx" as (γs) "[Hγs Hx]"; iDestruct "Hy" as (γs') "[Hγs' Hy]".
   iDestruct (own_valid_2 with "Hγs Hγs'") as %Hγs%auth_own_valid.
-  move: Hγs; rewrite /= op_singleton singleton_valid=> /agree_op_inv /(inj to_agree) [<-].
+  move: Hγs; rewrite /= op_singleton singleton_valid=> /agree_op_inv /(inj to_agree) <-.
   iExists γs. iSplit. done. rewrite own_op; iFrame.
 Qed.
 Global Instance own_bor_into_op κ x x1 x2 :
@@ -85,7 +85,7 @@ Proof.
   iIntros "[Hx Hy]".
   iDestruct "Hx" as (γs) "[Hγs Hx]"; iDestruct "Hy" as (γs') "[Hγs' Hy]".
   iDestruct (own_valid_2 with "Hγs Hγs'") as %Hγs%auth_own_valid.
-  move: Hγs; rewrite /= op_singleton singleton_valid=> /agree_op_inv /(inj to_agree) [<-].
+  move: Hγs; rewrite /= op_singleton singleton_valid=> /agree_op_inv /(inj to_agree) <-.
   iExists γs. iSplit; first done. rewrite own_op; iFrame.
 Qed.
 Global Instance own_cnt_into_op κ x x1 x2 :
@@ -119,7 +119,7 @@ Proof.
   iIntros "[Hx Hy]".
   iDestruct "Hx" as (γs) "[Hγs Hx]"; iDestruct "Hy" as (γs') "[Hγs' Hy]".
   iDestruct (own_valid_2 with "Hγs Hγs'") as %Hγs%auth_own_valid.
-  move: Hγs; rewrite /= op_singleton singleton_valid=> /agree_op_inv /(inj to_agree) [<-].
+  move: Hγs; rewrite /= op_singleton singleton_valid=> /agree_op_inv /(inj to_agree) <-.
   iExists γs. iSplit. done. rewrite own_op; iFrame.
 Qed.
 Global Instance own_inh_into_op κ x x1 x2 :
-- 
GitLab