Commit 6f129507 authored by Ralf Jung's avatar Ralf Jung
Browse files

update dependencies

parent f2bf7831
......@@ -11,6 +11,6 @@ install: [make "install"]
remove: [ "sh" "-c" "rm -rf '%{lib}%/coq/user-contrib/iris_time" ]
depends: [
"coq" { (>= "8.10.2" & < "8.13~") | (= "dev") }
"coq-iris" { (= "dev.2021-09-01.0.55cd1cc9") | (= "dev") }
"coq-iris" { (= "dev.2021-12-09.1.f52f9f6a") | (= "dev") }
"coq-tlc" { (= "20200328") | (= "dev") }
]
......@@ -265,13 +265,13 @@ Section Translation.
destruct v1, v2 ; try done ;
simpl ; case_match ; try done ;
simpl ; case_match ; try done ;
repeat f_equal ; apply bool_decide_iff ; naive_solver.
repeat f_equal ; apply bool_decide_ext ; naive_solver.
Qed.
Local Lemma _bool_decide_eq_translationV v1 v2 :
bool_decide (v1 = v2) = bool_decide (translationV v1 = translationV v2).
Proof.
apply bool_decide_iff ; split ; intros H.
apply bool_decide_ext ; split ; intros H.
- by rewrite H.
- by eapply translationV_injective.
Qed.
......
......@@ -926,7 +926,7 @@ Proof using.
wp_apply (find_spec with "[//] [$TC1 $UF]")=>//. iIntros "UF".
wp_apply (find_spec with "[//] [$TC2 $UF]")=>//. iIntros "UF".
wp_tick_op.
rewrite (bool_decide_iff (#(R x) = #(R y)) (R x = R y)); last (split; congruence).
rewrite (bool_decide_ext (#(R x) = #(R y)) (R x = R y)); last (split; congruence).
by iApply "HΦ".
Qed.
......
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