From ea42f9947c8498292a0b02a3f901f0826b80ea63 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Thu, 24 Aug 2017 15:57:02 +0200
Subject: [PATCH] Fix spurious whitespace

Fixes #96
---
 theories/proofmode/notation.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/theories/proofmode/notation.v b/theories/proofmode/notation.v
index bd4273137..8e34280a8 100644
--- a/theories/proofmode/notation.v
+++ b/theories/proofmode/notation.v
@@ -7,7 +7,7 @@ Arguments Envs _ _%proof_scope _%proof_scope.
 Arguments Enil {_}.
 Arguments Esnoc {_} _%proof_scope _%string _%uPred_scope.
 
-Notation "" := Enil (format "", only printing) : proof_scope.
+Notation "" := Enil (only printing) : proof_scope.
 Notation "Γ H : P" := (Esnoc Γ H P)
   (at level 1, P at level 200,
    left associativity, format "Γ H  :  P '//'", only printing) : proof_scope.
-- 
GitLab