Commit 57485cae authored by Robbert Krebbers's avatar Robbert Krebbers

Revert "Add the zero-width spaces at the *end* of the lines, and a

newline before the first context" and "shuffle 0-width spaces around so
they are distributed more evenly"

This reverts commits e3c56f9e and
7fc1124c, which are workarounds for
Coq bug https://coq.inria.fr/bugs/show_bug.cgi?id=4675

Also, this commit fixes the levels to avoid parantheses.
parent 4b0dd0df
......@@ -7,21 +7,21 @@ Arguments Enil {_}.
Arguments Esnoc {_} _%proof_scope _%string _%uPred_scope.
Notation "​" := Enil (format "​") : proof_scope.
Notation "Γ ​ H : P" := (Esnoc Γ H P)
Notation "​ Γ H : P" := (Esnoc Γ H P)
(at level 1, P at level 200,
left associativity, format "Γ ​ '//' H : P") : proof_scope.
left associativity, format "​ Γ H : P '//'") : proof_scope.
Notation "Γ '--------------------------------------' □ Δ '--------------------------------------' ★ Q" :=
(of_envs (Envs Γ Δ) Q%I)
(at level 1, Q at level 200, left associativity,
format "Γ '//' '--------------------------------------' □ Δ '//' '--------------------------------------' ★ '//' Q '//'") :
format "Γ '--------------------------------------' □ '//' Δ '--------------------------------------' ★ '//' Q '//'") :
C_scope.
Notation "Δ '--------------------------------------' ★ Q" :=
(of_envs (Envs Enil Δ) Q%I)
(at level 1, Q at level 200, left associativity,
format "Δ '//' '--------------------------------------' ★ '//' Q '//'") : C_scope.
format "Δ '--------------------------------------' ★ '//' Q '//'") : C_scope.
Notation "Γ '--------------------------------------' □ Q" :=
(of_envs (Envs Γ Enil) Q%I)
(at level 1, Q at level 200, left associativity,
format "Γ '//' '--------------------------------------' □ '//' Q '//'") : C_scope.
format "Γ '--------------------------------------' □ '//' Q '//'") : C_scope.
Notation "​​ Q" := (of_envs (Envs Enil Enil) Q%I)
(at level 1, format "​​ Q") : C_scope.
(at level 1, Q at level 200, format "​​ Q") : 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