diff --git a/theories/proofmode/notation.v b/theories/proofmode/notation.v
index 562d19ee756326a4c86302b492db8f1fa598a2b1..bd4273137e2f8a9dadca887450ec6ef819a81028 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.