From ce5f7710140bcac5abf42d07a32331890073a977 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 25 Aug 2016 18:14:17 +0200
Subject: [PATCH] Also use %E scopes in notations for Hoare triples.

---
 program_logic/hoare.v | 16 ++++++++--------
 1 file changed, 8 insertions(+), 8 deletions(-)

diff --git a/program_logic/hoare.v b/program_logic/hoare.v
index 95c58f4cb..817a21e29 100644
--- a/program_logic/hoare.v
+++ b/program_logic/hoare.v
@@ -6,29 +6,29 @@ Definition ht `{irisG Λ Σ} (E : coPset) (P : iProp Σ)
   (□ (P → WP e @ E {{ Φ }}))%I.
 Instance: Params (@ht) 4.
 
-Notation "{{ P } } e @ E {{ Φ } }" := (ht E P e Φ)
+Notation "{{ P } } e @ E {{ Φ } }" := (ht E P e%E Φ)
   (at level 20, P, e, Φ at level 200,
    format "{{  P  } }  e  @  E  {{  Φ  } }") : uPred_scope.
-Notation "{{ P } } e {{ Φ } }" := (ht ⊤ P e Φ)
+Notation "{{ P } } e {{ Φ } }" := (ht ⊤ P e%E Φ)
   (at level 20, P, e, Φ at level 200,
    format "{{  P  } }  e  {{  Φ  } }") : uPred_scope.
-Notation "{{ P } } e @ E {{ Φ } }" := (True ⊢ ht E P e Φ)
+Notation "{{ P } } e @ E {{ Φ } }" := (True ⊢ ht E P e%E Φ)
   (at level 20, P, e, Φ at level 200,
    format "{{  P  } }  e  @  E  {{  Φ  } }") : C_scope.
-Notation "{{ P } } e {{ Φ } }" := (True ⊢ ht ⊤ P e Φ)
+Notation "{{ P } } e {{ Φ } }" := (True ⊢ ht ⊤ P e%E Φ)
   (at level 20, P, e, Φ at level 200,
    format "{{  P  } }  e  {{  Φ  } }") : C_scope.
 
-Notation "{{ P } } e @ E {{ v , Q } }" := (ht E P e (λ v, Q))
+Notation "{{ P } } e @ E {{ v , Q } }" := (ht E P e%E (λ v, Q))
   (at level 20, P, e, Q at level 200,
    format "{{  P  } }  e  @  E  {{  v ,  Q  } }") : uPred_scope.
-Notation "{{ P } } e {{ v , Q } }" := (ht ⊤ P e (λ v, Q))
+Notation "{{ P } } e {{ v , Q } }" := (ht ⊤ P e%E (λ v, Q))
   (at level 20, P, e, Q at level 200,
    format "{{  P  } }  e  {{  v ,  Q  } }") : uPred_scope.
-Notation "{{ P } } e @ E {{ v , Q } }" := (True ⊢ ht E P e (λ v, Q))
+Notation "{{ P } } e @ E {{ v , Q } }" := (True ⊢ ht E P e%E (λ v, Q))
   (at level 20, P, e, Q at level 200,
    format "{{  P  } }  e  @  E  {{  v ,  Q  } }") : C_scope.
-Notation "{{ P } } e {{ v , Q } }" := (True ⊢ ht ⊤ P e (λ v, Q))
+Notation "{{ P } } e {{ v , Q } }" := (True ⊢ ht ⊤ P e%E (λ v, Q))
   (at level 20, P, e, Q at level 200,
    format "{{  P  } }  e  {{  v ,  Q  } }") : C_scope.
 
-- 
GitLab