From b00ace043411571105cc88c5208af8be4ef80b39 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Wed, 7 Dec 2016 10:57:33 +0100
Subject: [PATCH] Mark notation as "only printing"

Unfortunately, we currently have to keep the unicode-space hack in some places because Coq still complains about the notation otherwise
---
 theories/proofmode/notation.v | 14 +++++++-------
 1 file changed, 7 insertions(+), 7 deletions(-)

diff --git a/theories/proofmode/notation.v b/theories/proofmode/notation.v
index 57b08033b..ae9313713 100644
--- a/theories/proofmode/notation.v
+++ b/theories/proofmode/notation.v
@@ -7,22 +7,22 @@ Arguments Envs _ _%proof_scope _%proof_scope.
 Arguments Enil {_}.
 Arguments Esnoc {_} _%proof_scope _%string _%uPred_scope.
 
-Notation "​" := Enil (format "​") : proof_scope.
-Notation "Γ ​ H : P" := (Esnoc Γ H P)
+Notation "​" := Enil (format "​", only printing) : proof_scope.
+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 '//'", only printing) : proof_scope.
 Notation "Γ '--------------------------------------' □ Δ '--------------------------------------' ∗ Q" :=
   (of_envs (Envs Γ Δ) ⊢ Q%I)
   (at level 1, Q at level 200, left associativity,
-  format "Γ '--------------------------------------' □ '//' Δ '--------------------------------------' ∗ '//' Q '//'") :
+  format "Γ '--------------------------------------' □ '//' Δ '--------------------------------------' ∗ '//' Q '//'", only printing) :
   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 '//'", only printing) : 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 '//'", only printing)  : C_scope.
 Notation "​​ Q" := (of_envs (Envs Enil Enil) ⊢ Q%I)
-  (at level 1, Q at level 200, format "​​ Q") : C_scope.
+  (at level 1, Q at level 200, format "​​ Q", only printing) : C_scope.
-- 
GitLab