Skip to content
Snippets Groups Projects
Commit eb203c6b authored by Jacques-Henri Jourdan's avatar Jacques-Henri Jourdan
Browse files

Tweak.

parent c1196f5e
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
Showing
with 1 addition and 1 deletion
theories/bi/monpred.v
+ 1
− 1
View file @ eb203c6b
...@@ -500,7 +500,7 @@ Global Instance monPred_car_timeless P i : Timeless P → Timeless (P i). ...@@ -500,7 +500,7 @@ Global Instance monPred_car_timeless P i : Timeless P → Timeless (P i).
Proof. move => [] /(_ i). unfold Timeless. by unseal. Qed. Proof. move => [] /(_ i). unfold Timeless. by unseal. Qed.
Global Instance monPred_ipure_timeless (P : PROP) : Global Instance monPred_ipure_timeless (P : PROP) :
Timeless P → @Timeless (monPredSI I PROP) ⎡P⎤%I. Timeless P → @Timeless (monPredSI I PROP) ⎡P⎤%I.
Proof. intros. split => ? /=. unseal. exact: H. Qed. Proof. intros. split => ? /=. by unseal. Qed.
Global Instance monPred_in_timeless i0 : Timeless (@monPred_in I PROP i0). Global Instance monPred_in_timeless i0 : Timeless (@monPred_in I PROP i0).
Proof. split => ? /=. unseal. apply timeless, _. Qed. Proof. split => ? /=. unseal. apply timeless, _. Qed.
Global Instance monPred_all_timeless P : Global Instance monPred_all_timeless P :
......
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