Commit e5c51505 authored by Jacques-Henri Jourdan's avatar Jacques-Henri Jourdan
Browse files

Make iFrame able to strip a later from a framed hypothesis when framing under a later.

parent fdb79e2c
...@@ -1472,6 +1472,7 @@ Qed. ...@@ -1472,6 +1472,7 @@ Qed.
Theorem soundness : ¬ (True False). Theorem soundness : ¬ (True False).
Proof. exact (adequacy False 0). Qed. Proof. exact (adequacy False 0). Qed.
End uPred_logic. End uPred_logic.
(* Hint DB for the logic *) (* Hint DB for the logic *)
......
...@@ -269,10 +269,10 @@ Proof. by rewrite /MakeLater later_True. Qed. ...@@ -269,10 +269,10 @@ Proof. by rewrite /MakeLater later_True. Qed.
Global Instance make_later_default P : MakeLater P ( P) | 100. Global Instance make_later_default P : MakeLater P ( P) | 100.
Proof. done. Qed. Proof. done. Qed.
Global Instance frame_later R P Q Q' : Global Instance frame_later R R' P Q Q' :
Frame R P Q MakeLater Q Q' Frame R ( P) Q'. Frame R P Q MakeLater Q Q' IntoLater R' R Frame R' ( P) Q'.
Proof. Proof.
rewrite /Frame /MakeLater=><- <-. by rewrite later_sep -(later_intro R). rewrite /Frame /MakeLater /IntoLater=><- <- ->. by rewrite later_sep.
Qed. Qed.
Class MakeExceptLast (P Q : uPred M) := make_except_last : P ⊣⊢ Q. Class MakeExceptLast (P Q : uPred M) := make_except_last : P ⊣⊢ Q.
......
Supports Markdown
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