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

Fix CI.

parent d50619d0
......@@ -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-04-19.0.9e4493f9") | (= "dev") }
"coq-iris" { (= "dev.2021-05-07.0.5119ab8b") | (= "dev") }
"coq-tlc" { (= "20200328") | (= "dev") }
]
......@@ -10,7 +10,6 @@ Open Scope Z_scope.
*)
Section clock_int.
Context `{timeReceiptHeapG Σ}.
Context (nmax : nat).
Context `(nmax max_mach_int).
......@@ -39,9 +38,8 @@ Section clock_int.
iDestruct ("Post" with "[H]") as "Post".
{ iIntros "{$H} !%". lia. }
wp_tick_op=>//.
by rewrite /bin_op_eval /= /to_mach_int /mach_int_bounded decide_left.
by rewrite /bin_op_eval /= /to_mach_int /mach_int_bounded decide_True_pi.
Qed.
End clock_int.
(*
......@@ -80,7 +78,7 @@ Section snapclock_int.
(* FIXME : why isn't lia able to do this directly? *)
trans 0. unfold min_mach_int; lia. lia. }
wp_tick_op.
{ by rewrite /bin_op_eval /= /to_mach_int /mach_int_bounded decide_left. }
{ by rewrite /bin_op_eval /= /to_mach_int /mach_int_bounded decide_True_pi. }
iApply "Post". iSplit. auto with lia.
rewrite Z2Nat.inj_add // Nat.add_comm //.
Qed.
......@@ -107,7 +105,6 @@ Section snapclock_int.
iDestruct ("Post" with "[H]") as "Post".
{ iSplit; auto with lia. }
wp_tick_op=>//.
by rewrite /bin_op_eval /= /to_mach_int /mach_int_bounded decide_left.
by rewrite /bin_op_eval /= /to_mach_int /mach_int_bounded decide_True_pi.
Qed.
End snapclock_int.
......@@ -755,7 +755,7 @@ Proof using.
repeat iSplit; try iPureIntro.
{ applys* Inv_make. } { applys* Mem_make. }
iApply mapsto_M_insert; [done| |by iFrame].
rewrite /= /to_mach_int decide_left /=; [by apply (proj2_sig mach_int_0)|].
rewrite /= /to_mach_int decide_True_pi /=; [by apply (proj2_sig mach_int_0)|].
intros ?. by rewrite (exists_proj1_pi _ mach_int_0).
Qed.
......@@ -1036,7 +1036,7 @@ Proof using.
assert (`k1 = `k1') as -> by lia. rewrite (_:`k1' = K y) //.
rewrite Z.add_comm -(Nat2Z.inj_add 1). done. }
wp_tick_seq. wp_tick_op.
{ by rewrite /bin_op_eval /= /to_mach_int decide_left. }
{ by rewrite /bin_op_eval /= /to_mach_int decide_True_pi. }
iDestruct (mapsto_M_acc _ x with "HM") as (v'' Hv'') "[Hx HM]".
{ rewrite lookup_insert_ne //. congruence. }
wp_tick_pair. wp_tick_inj. wp_tick_store. wp_tick_seq.
......@@ -1047,7 +1047,7 @@ Proof using.
iSplit; last iApply ("HM" with "[%] Hx").
{ iPureIntro. applys* Mem_link_incr HM. congruence. applys update2_sym. }
rewrite /= -(_:(`k1 + 1) = (K y + 1)%nat) //.
{ by rewrite /to_mach_int decide_left /=. }
{ by rewrite /to_mach_int decide_True_pi /=. }
assert (`k1 + 1 = K y + 1)%Z as -> by lia. by rewrite ->Nat2Z.inj_add. }
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