Commit f6f511e6 authored by Ralf Jung's avatar Ralf Jung

use coq 8.6 mode '!' to fix diverging apply:

There are certainly more places this is useful, but let's start with this simple test
parent 8706664d
......@@ -33,6 +33,7 @@ Class TimelessP {M} (P : uPred M) := timelessP : ▷ P ⊢ ◇ P.
Arguments timelessP {_} _ {_}.
Class PersistentP {M} (P : uPred M) := persistentP : P P.
Hint Mode PersistentP - ! : typeclass_instances.
Arguments persistentP {_} _ {_}.
Module uPred.
......
......@@ -104,7 +104,7 @@ Proof. apply wand_intro_r. by rewrite -own_op own_valid. Qed.
Lemma own_valid_3 γ a1 a2 a3 : own γ a1 - own γ a2 - own γ a3 - (a1 a2 a3).
Proof. do 2 apply wand_intro_r. by rewrite -!own_op own_valid. Qed.
Lemma own_valid_r γ a : own γ a own γ a a.
Proof. apply (uPred.always_entails_r _ _). apply own_valid. Qed.
Proof. apply: uPred.always_entails_r. apply own_valid. Qed.
Lemma own_valid_l γ a : own γ a a own γ a.
Proof. by rewrite comm -own_valid_r. Qed.
......
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