From c9ae33d42e2014b8f228cff640a072a3469b0b90 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Mon, 18 Jan 2016 02:52:59 +0100
Subject: [PATCH] Fix typo in scopes for notations of triples.

---
 iris/hoare.v | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/iris/hoare.v b/iris/hoare.v
index a52f50f7d..018f8858a 100644
--- a/iris/hoare.v
+++ b/iris/hoare.v
@@ -6,9 +6,9 @@ Definition ht {Σ} (E : coPset) (P : iProp Σ)
 Instance: Params (@ht) 2.
 
 Notation "{{ P } } e @ E {{ Q } }" := (ht E P e Q)
-  (at level 74, format "{{  P  } }  e  @  E  {{  Q  } }") : C_scope.
+  (at level 74, format "{{  P  } }  e  @  E  {{  Q  } }") : uPred_scope.
 Notation "{{ P } } e @ E {{ Q } }" := (True ⊑ ht E P e Q)
-  (at level 74, format "{{  P  } }  e  @  E  {{  Q  } }") : type_scope.
+  (at level 74, format "{{  P  } }  e  @  E  {{  Q  } }") : C_scope.
 
 Section hoare.
 Context {Σ : iParam}.
-- 
GitLab