From 8d6285407e6c3088f8b5719e9fc7bdd40cd66e39 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Mon, 19 Feb 2018 09:56:31 +0100
Subject: [PATCH] Remove useless new line.

---
 theories/proofmode/tactics.v | 1 -
 1 file changed, 1 deletion(-)

diff --git a/theories/proofmode/tactics.v b/theories/proofmode/tactics.v
index 186e1dda9..37eaf0a8c 100644
--- a/theories/proofmode/tactics.v
+++ b/theories/proofmode/tactics.v
@@ -1903,5 +1903,4 @@ Hint Extern 1 (envs_entails _ (_ ∨ _)) => iRight.
 Hint Extern 1 (envs_entails _ (|==> _)) => iModIntro.
 Hint Extern 2 (envs_entails _ (|={_}=> _)) => iModIntro.
 
-
 Hint Extern 2 (envs_entails _ (_ ∗ _)) => progress iFrame : iFrame.
-- 
GitLab