Commit 2a7755fe authored by Robbert Krebbers's avatar Robbert Krebbers

Different treatment of atomic premise in type class.

In Coq 8.6 type class search is not called recursively on premises
that are not type classes. To that end, we use a hint extern to invoke
an ordinary auto.
parent 599d7411
Pipeline #3005 passed with stage
in 10 minutes
......@@ -230,7 +230,7 @@ Ltac solve_atomic :=
end.
Hint Extern 10 (language.atomic _) => solve_atomic.
(* For the side-condition of elim_upd_fupd_wp_atomic *)
Hint Extern 10 (language.atomic _) => solve_atomic : typeclass_instances.
Hint Extern 10 (language.atomic _) => solve_atomic : atomic.
(** Substitution *)
Ltac simpl_subst :=
......
......@@ -310,12 +310,13 @@ Section proofmode_classes.
ElimModal (|={E}=> P) P (WP e @ E {{ Φ }}) (WP e @ E {{ Φ }}).
Proof. by rewrite /ElimModal fupd_frame_r wand_elim_r fupd_wp. Qed.
(* lower precedence, if possible, it should always pick elim_upd_fupd_wp *)
Global Instance elim_modal_fupd_wp_atomic E1 E2 e P Φ :
Instance elim_modal_fupd_wp_atomic E1 E2 e P Φ :
atomic e
ElimModal (|={E1,E2}=> P) P
(WP e @ E1 {{ Φ }}) (WP e @ E2 {{ v, |={E2,E1}=> Φ v }})%I | 100.
Proof. intros. by rewrite /ElimModal fupd_frame_r wand_elim_r wp_atomic. Qed.
End proofmode_classes.
Hint Extern 0 (atomic _) => assumption : typeclass_instances.
(* Lower precedence, if possible, it should always pick elim_upd_fupd_wp *)
Hint Extern 100 (ElimModal (|={_,_}=> _) _ (WP _ @ _ {{ _ }}) _) =>
eapply elim_modal_fupd_wp_atomic; solve [auto with atomic] : typeclass_instances.
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