Skip to content
Snippets Groups Projects
Commit facc4127 authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

FromPure instance for later, to make iPureIntro/done work on laters.

parent 293fb6c7
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
theories/proofmode/class_instances.v
+ 3
− 0
View file @ facc4127
...@@ -124,6 +124,9 @@ Proof. ...@@ -124,6 +124,9 @@ Proof.
rewrite -Hx. apply pure_intro. done. rewrite -Hx. apply pure_intro. done.
Qed. Qed.
Global Instance from_pure_later P φ : FromPure P φ → FromPure (▷ P)%I φ.
Proof. rewrite /FromPure=> ->. apply later_intro. Qed.
(* IntoPersistentP *) (* IntoPersistentP *)
Global Instance into_persistentP_always_trans P Q : Global Instance into_persistentP_always_trans P Q :
IntoPersistentP P Q → IntoPersistentP (□ P) Q | 0. IntoPersistentP P Q → IntoPersistentP (□ P) Q | 0.
......
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