diff --git a/theories/proofmode/notation.v b/theories/proofmode/notation.v
index 8a13dcaf81cb946e8830a3aa2422051b7be2f8e7..562d19ee756326a4c86302b492db8f1fa598a2b1 100644
--- a/theories/proofmode/notation.v
+++ b/theories/proofmode/notation.v
@@ -24,5 +24,5 @@ Notation "Γ '--------------------------------------' □ Q" :=
   (of_envs (Envs Γ Enil) ⊢ Q%I)
   (at level 1, Q at level 200, left associativity,
   format "Γ '--------------------------------------' □ '//' Q '//'", only printing)  : C_scope.
-Notation "⊢ Q" := (of_envs (Envs Enil Enil) ⊢ Q%I)
-  (at level 1, Q at level 200, format "⊢  Q", only printing) : C_scope.
+Notation "'--------------------------------------' ∗ Q" := (of_envs (Envs Enil Enil) ⊢ Q%I)
+  (at level 1, Q at level 200, format "'--------------------------------------' ∗ '//' Q '//'", only printing) : C_scope.