From 59a14ac3eb8c89759afa5ae45790d109ded5850b Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Sat, 5 Sep 2020 14:52:58 +0200
Subject: [PATCH] Redundant space.

---
 tests/proofmode_siprop.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/tests/proofmode_siprop.v b/tests/proofmode_siprop.v
index 1788f69c4..57e9a7332 100644
--- a/tests/proofmode_siprop.v
+++ b/tests/proofmode_siprop.v
@@ -1,4 +1,4 @@
-From iris.proofmode Require Import tactics .
+From iris.proofmode Require Import tactics.
 From iris.si_logic Require Import bi.
 
 Section si_logic_tests.
-- 
GitLab