From 293fb6c770876069a66e19d5c0390121f69e3f49 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Wed, 26 Apr 2017 17:51:27 +0200
Subject: [PATCH] Fix bug #85 in another way.

After discussing this with Ralf, again, it turned out that using a bar
instead of a turnstyle would be better. When formalizing type systems, one
often wants to use a turnstyle in other notations (the typing judgment),
so having the turnstyle in the proofmode notation is confusing.
---
 theories/proofmode/notation.v | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/theories/proofmode/notation.v b/theories/proofmode/notation.v
index 8a13dcaf8..562d19ee7 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.
-- 
GitLab