From 191c8f1750eef51409533f0792506878d6edc2a1 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Wed, 10 Feb 2016 01:19:03 +0100
Subject: [PATCH] Change the level of wand so it is more like the implication.

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

diff --git a/algebra/upred.v b/algebra/upred.v
index 146d71c67..cbe1f822e 100644
--- a/algebra/upred.v
+++ b/algebra/upred.v
@@ -220,7 +220,7 @@ Infix "→" := uPred_impl : uPred_scope.
 Infix "★" := uPred_sep (at level 80, right associativity) : uPred_scope.
 Notation "(★)" := uPred_sep (only parsing) : uPred_scope.
 Notation "P -★ Q" := (uPred_wand P Q)
-  (at level 90, Q at level 200, right associativity) : uPred_scope.
+  (at level 199, Q at level 200, right associativity) : uPred_scope.
 Notation "∀ x .. y , P" :=
   (uPred_forall (λ x, .. (uPred_forall (λ y, P)) ..)%I) : uPred_scope.
 Notation "∃ x .. y , P" :=
-- 
GitLab