From 9fdbbf4b5665c7daa95b62083693d43c93b38b45 Mon Sep 17 00:00:00 2001 From: Jacques-Henri Jourdan <jacques-henri.jourdan@normalesup.org> Date: Tue, 16 Jan 2018 18:56:23 +0100 Subject: [PATCH] AddModal: fix priorities. --- theories/proofmode/class_instances.v | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/theories/proofmode/class_instances.v b/theories/proofmode/class_instances.v index 546c65c07..b8b184c06 100644 --- a/theories/proofmode/class_instances.v +++ b/theories/proofmode/class_instances.v @@ -909,12 +909,12 @@ Proof. intros. rewrite /AddModal (except_0_intro (_ -∗ _)) (timeless P). by rewrite -except_0_sep wand_elim_r except_0_later. Qed. -Global Instance add_modal_except_0 P Q : AddModal (◇ P) P (◇ Q). +Global Instance add_modal_except_0 P Q : AddModal (◇ P) P (◇ Q) | 1. Proof. intros. rewrite /AddModal (except_0_intro (_ -∗ _)). by rewrite -except_0_sep wand_elim_r except_0_idemp. Qed. -Global Instance add_modal_except_0_later P Q : AddModal (◇ P) P (▷ Q). +Global Instance add_modal_except_0_later P Q : AddModal (◇ P) P (▷ Q) | 1. Proof. intros. rewrite /AddModal (except_0_intro (_ -∗ _)). by rewrite -except_0_sep wand_elim_r except_0_later. -- GitLab