Commit 293fb6c7 authored by Robbert Krebbers's avatar Robbert Krebbers

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.
parent 558b080f
......@@ -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.
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment