Commit a9880321 authored by Jacques-Henri Jourdan's avatar Jacques-Henri Jourdan

Higher cost for [elim_modal_fupd_fupd to give priority on [elim_modal_step_fupd.

parent f49a7f18
Pipeline #3188 failed with stage
in 3 minutes
...@@ -179,9 +179,9 @@ Section proofmode_classes. ...@@ -179,9 +179,9 @@ Section proofmode_classes.
ElimModal (|==> P) P (|={E1,E2}=> Q) (|={E1,E2}=> Q). ElimModal (|==> P) P (|={E1,E2}=> Q) (|={E1,E2}=> Q).
Proof. Proof.
by rewrite /ElimModal (bupd_fupd E1) fupd_frame_r wand_elim_r fupd_trans. by rewrite /ElimModal (bupd_fupd E1) fupd_frame_r wand_elim_r fupd_trans.
Qed. Qed.
Global Instance elim_modal_fupd_fupd E1 E2 E3 P Q : Global Instance elim_modal_fupd_fupd E1 E2 E3 P Q :
ElimModal (|={E1,E2}=> P) P (|={E1,E3}=> Q) (|={E2,E3}=> Q). ElimModal (|={E1,E2}=> P) P (|={E1,E3}=> Q) (|={E2,E3}=> Q) | 10.
Proof. by rewrite /ElimModal fupd_frame_r wand_elim_r fupd_trans. Qed. Proof. by rewrite /ElimModal fupd_frame_r wand_elim_r fupd_trans. Qed.
End proofmode_classes. End proofmode_classes.
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment