From fab931300becdb4d58ec33b0d18b8d3f767102f5 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Tue, 22 Aug 2017 13:33:30 +0200
Subject: [PATCH] get rid of the remaining empty-unicode-space hacks

---
 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 562d19ee7..bd4273137 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 (format "", 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