From eb7a762b98c526d540487c80381ee5710daa2ed9 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Wed, 1 Jun 2016 13:57:18 +0200
Subject: [PATCH] Change the Coq scope notations for viewshifts into parsing
 only.

They mess up the proof mode notations due to overlaps.
---
 program_logic/pviewshifts.v | 6 ++----
 1 file changed, 2 insertions(+), 4 deletions(-)

diff --git a/program_logic/pviewshifts.v b/program_logic/pviewshifts.v
index 3aaa3521a..f045dc2c0 100644
--- a/program_logic/pviewshifts.v
+++ b/program_logic/pviewshifts.v
@@ -41,11 +41,9 @@ Notation "|==> Q" := (pvs ⊤ ⊤ Q%I)
   (at level 99, Q at level 200, format "|==>  Q") : uPred_scope.
 
 Notation "P ={ E1 , E2 }=> Q" := (P ⊢ |={E1,E2}=> Q)
-  (at level 99, E1, E2 at level 50, Q at level 200,
-   format "P  ={ E1 , E2 }=>  Q") : C_scope.
+  (at level 99, E1, E2 at level 50, Q at level 200, only parsing) : C_scope.
 Notation "P ={ E }=> Q" := (P ⊢ |={E}=> Q)
-  (at level 99, E at level 50, Q at level 200,
-   format "P  ={ E }=>  Q") : C_scope.
+  (at level 99, E at level 50, Q at level 200, only parsing) : C_scope.
 
 Section pvs.
 Context {Λ : language} {Σ : iFunctor}.
-- 
GitLab