From bbda866bd84ea503a56739dd92be1da647177002 Mon Sep 17 00:00:00 2001
From: Jacques-Henri Jourdan <jjourdan@mpi-sws.org>
Date: Thu, 18 Aug 2016 16:32:53 +0200
Subject: [PATCH] USeless spaces
---
program_logic/thread_local.v | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/program_logic/thread_local.v b/program_logic/thread_local.v
index 882fb3872..86db05b0a 100644
--- a/program_logic/thread_local.v
+++ b/program_logic/thread_local.v
@@ -80,7 +80,7 @@ Section proofs.
iIntros (??) "#Htlinv Htoks".
iDestruct "Htlinv" as (i) "[% #Hinv]".
rewrite {1 4}(union_difference_L (nclose N) E) //.
- rewrite {1 5}(union_difference_L {[i]} (nclose N)) ?tl_tokens_union; try set_solver.
+ rewrite {1 5}(union_difference_L {[i]} (nclose N)) ?tl_tokens_union; try set_solver.
iDestruct "Htoks" as "[[Htoki Htoks0] Htoks1]". iFrame "Htoks0 Htoks1".
iInv tlN as "[[HP >Hdis]|>Htoki2]" "Hclose".
- iVs ("Hclose" with "[Htoki]") as "_". auto. iFrame.
--
GitLab