From 57485cae355ca824435194cd64de2eb22bb26f0c Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Mon, 18 Apr 2016 22:48:29 +0200
Subject: [PATCH] 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 e3c56f9e10ea47cbf767516b1967af9dc8be7eaa and
7fc1124c52549bea9cc5e963f284b26ec249364b, 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.
---
 proofmode/notation.v | 12 ++++++------
 1 file changed, 6 insertions(+), 6 deletions(-)

diff --git a/proofmode/notation.v b/proofmode/notation.v
index 85f7a804c..f1c6a2663 100644
--- a/proofmode/notation.v
+++ b/proofmode/notation.v
@@ -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.
-- 
GitLab