From d0733ad860ab42d4dfe3c7c7e14bbbb84ef82b05 Mon Sep 17 00:00:00 2001 From: Ralf Jung <jung@mpi-sws.org> Date: Fri, 15 Apr 2016 12:58:19 +0200 Subject: [PATCH] shuffle 0-width spaces around so they are distributed more evenly FDor editors that display 0-width space with more than 0 width, this makes the indentation of assertions more consistent --- proofmode/notation.v | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/proofmode/notation.v b/proofmode/notation.v index f1c6a2663..638cf631d 100644 --- a/proofmode/notation.v +++ b/proofmode/notation.v @@ -7,9 +7,9 @@ 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, -- GitLab