From f0f8f422d5044320e9092c56b34ef8d6747ac7fe Mon Sep 17 00:00:00 2001
From: David Swasey <swasey@mpi-sws.org>
Date: Mon, 2 Feb 2015 15:56:13 +0100
Subject: [PATCH] Typos in (unused) notation.

---
 iris_core.v | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/iris_core.v b/iris_core.v
index 2557b9fbf..8ef4c23d3 100644
--- a/iris_core.v
+++ b/iris_core.v
@@ -153,9 +153,9 @@ Module IrisCore (RL : PCM_T) (C : CORE_LANG).
   Notation "p → q" := (BI.impl p q : Props) (at level 55, right associativity) : iris_scope.
   Notation "p '-*' q" := (si p q : Props) (at level 55, right associativity) : iris_scope.
   Notation "∀ x , p" := (all n[(fun x => p)] : Props) (at level 60, x ident, no associativity) : iris_scope.
-  Notation "∃ x , p" := (all n[(fun x => p)] : Props) (at level 60, x ident, no associativity) : iris_scope.
+  Notation "∃ x , p" := (xist n[(fun x => p)] : Props) (at level 60, x ident, no associativity) : iris_scope.
   Notation "∀ x : T , p" := (all n[(fun x : T => p)] : Props) (at level 60, x ident, no associativity) : iris_scope.
-  Notation "∃ x : T , p" := (all n[(fun x : T => p)] : Props) (at level 60, x ident, no associativity) : iris_scope.
+  Notation "∃ x : T , p" := (xist n[(fun x : T => p)] : Props) (at level 60, x ident, no associativity) : iris_scope.
 
   Lemma valid_iff p :
     valid p <-> (⊤ ⊑ p).
-- 
GitLab