Add visible notation for empty context in proofmode

Fixes issue #85

Add visible notation for empty context in proofmode
Fixes issue #85
36b9a605 · Ralf Jung · 0429c257 · 36b9a605
Commit 36b9a605 authored Mar 30, 2017 by Ralf Jung
Hide whitespace changes
Inline Side-by-side

Showing with 2 additions and 2 deletions

theories/proofmode/notation.v theories/proofmode/notation.v +2 -2

No files found.
--- 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.