Commit 4ffff895 authored by Robbert's avatar Robbert

Merge branch 'ci/robbert/no_backtracking' into 'master'

Use `NoBackTrack` type class for framing with ▷

Closes #153

See merge request FP/iris-coq!112
parents ae3b6560 5e3416d3
......@@ -12,5 +12,5 @@ remove: ["rm" "-rf" "%{lib}%/coq/user-contrib/iris"]
depends: [
"coq" { (>= "8.6.1" & < "8.8~") | (= "dev") }
"coq-mathcomp-ssreflect" { (>= "1.6.1" & < "1.7~") | (= "dev") }
"coq-stdpp" { (= "dev.2018-02-02.0") | (= "dev") }
"coq-stdpp" { (= "dev.2018-02-08.0") | (= "dev") }
]
......@@ -638,9 +638,10 @@ Global Instance make_later_default P : MakeLater P (▷ P) | 100.
Proof. done. Qed.
Global Instance frame_later p R R' P Q Q' :
IntoLaterN 1 R' R Frame p R P Q MakeLater Q Q' Frame p R' ( P) Q'.
NoBackTrack (IntoLaterN 1 R' R)
Frame p R P Q MakeLater Q Q' Frame p R' ( P) Q'.
Proof.
rewrite /Frame /MakeLater /IntoLaterN=>-> <- <-.
rewrite /Frame /MakeLater /IntoLaterN=>-[->] <- <-.
by rewrite persistently_if_later later_sep.
Qed.
......@@ -651,9 +652,10 @@ Global Instance make_laterN_default P : MakeLaterN n P (▷^n P) | 100.
Proof. done. Qed.
Global Instance frame_laterN p n R R' P Q Q' :
IntoLaterN n R' R Frame p R P Q MakeLaterN n Q Q' Frame p R' (^n P) Q'.
NoBackTrack (IntoLaterN n R' R)
Frame p R P Q MakeLaterN n Q Q' Frame p R' (^n P) Q'.
Proof.
rewrite /Frame /MakeLater /IntoLaterN=>-> <- <-.
rewrite /Frame /MakeLater /IntoLaterN=>-[->] <- <-.
by rewrite persistently_if_laterN laterN_sep.
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