From ff9ebff83744e71497dade8369cc78e8fd5e587c Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Mon, 8 Feb 2016 23:04:30 +0100
Subject: [PATCH] Fix scope for uPred_const.

---
 program_logic/upred.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/program_logic/upred.v b/program_logic/upred.v
index 7bafefba9..12df00e7a 100644
--- a/program_logic/upred.v
+++ b/program_logic/upred.v
@@ -208,7 +208,7 @@ Arguments uPred_holds {_} _%I _ _.
 Arguments uPred_entails _ _%I _%I.
 Notation "P ⊑ Q" := (uPred_entails P%I Q%I) (at level 70) : C_scope.
 Notation "(⊑)" := uPred_entails (only parsing) : C_scope.
-Notation "■ φ" := (uPred_const φ) (at level 20) : uPred_scope.
+Notation "■ φ" := (uPred_const φ%type) (at level 20) : uPred_scope.
 Notation "'False'" := (uPred_const False) : uPred_scope.
 Notation "'True'" := (uPred_const True) : uPred_scope.
 Infix "∧" := uPred_and : uPred_scope.
-- 
GitLab