From ab1632d3e096a4acd6540a1f020bab29af8846c6 Mon Sep 17 00:00:00 2001 From: Ralf Jung Date: Thu, 27 Oct 2016 11:09:33 +0200 Subject: [PATCH] repeat notation annotations for quantifiers, just to be sure --- base_logic/primitive.v | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/base_logic/primitive.v b/base_logic/primitive.v index 7bcce8d77..a7c13e15f 100644 --- a/base_logic/primitive.v +++ b/base_logic/primitive.v @@ -171,9 +171,11 @@ Notation "(★)" := uPred_sep (only parsing) : uPred_scope. Notation "P -★ Q" := (uPred_wand P Q) (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. + (uPred_forall (λ x, .. (uPred_forall (λ y, P)) ..)%I) + (at level 200, x binder, y binder, right associativity) : uPred_scope. Notation "∃ x .. y , P" := - (uPred_exist (λ x, .. (uPred_exist (λ y, P)) ..)%I) : uPred_scope. + (uPred_exist (λ x, .. (uPred_exist (λ y, P)) ..)%I) + (at level 200, x binder, y binder, right associativity) : uPred_scope. Notation "□ P" := (uPred_always P) (at level 20, right associativity) : uPred_scope. Notation "▷ P" := (uPred_later P) -- GitLab