From ebb20a1a1164020f82ab59fc4cb195af288d40a0 Mon Sep 17 00:00:00 2001 From: Robbert Krebbers <mail@robbertkrebbers.nl> Date: Thu, 7 Apr 2016 15:45:00 +0200 Subject: [PATCH] Fix level of magic wand. --- algebra/upred.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/algebra/upred.v b/algebra/upred.v index 76846af48..1005bf06f 100644 --- a/algebra/upred.v +++ b/algebra/upred.v @@ -286,7 +286,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 199, Q at level 200, right associativity) : uPred_scope. + (at level 99, 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