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