Attention une mise à jour du serveur va être effectuée le vendredi 16 avril entre 12h et 12h30. Cette mise à jour va générer une interruption du service de quelques minutes.

Commit 25decc5a authored by Jacques-Henri Jourdan's avatar Jacques-Henri Jourdan

Bump iris, change tac_wp_pure so that it does not require [pure_exec_fill]...

Bump iris, change tac_wp_pure so that it does not require [pure_exec_fill] being declared as an instance.
parent ffa94a95
......@@ -5,6 +5,8 @@ Makefile.coq
*.glob
*.vo
*.vio
*.vos
*.vok
.coqdeps.d
.lia.cache
*.tar.gz
......
......@@ -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.2020-11-13.0.88773f25") | (= "dev") }
"coq-iris" { (= "dev.2020-11-27.0.f0f9f3b6") | (= "dev") }
"coq-tlc" { (= "20200328") | (= "dev") }
]
......@@ -22,14 +22,16 @@ Tactic Notation "wp_expr_eval" tactic(t) :=
Ltac wp_expr_simpl := wp_expr_eval simpl.
Lemma tac_wp_pure `{heapG Σ} Δ Δ' s E e1 e2 φ n Φ :
Lemma tac_wp_pure `{heapG Σ} Δ Δ' s E K e1 e2 φ n Φ :
PureExec φ n e1 e2
φ
MaybeIntoLaterNEnvs n Δ Δ'
envs_entails Δ' (WP e2 @ s; E {{ Φ }})
envs_entails Δ (WP e1 @ s; E {{ Φ }}).
envs_entails Δ' (WP (fill K e2) @ s; E {{ Φ }})
envs_entails Δ (WP (fill K e1) @ s; E {{ Φ }}).
Proof.
rewrite envs_entails_eq=> ??? HΔ'. rewrite into_laterN_env_sound /=.
(* We want [pure_exec_fill] to be available to TC search locally. *)
pose proof @pure_exec_fill.
rewrite HΔ' -lifting.wp_pure_step_later //.
Qed.
......@@ -47,7 +49,7 @@ Tactic Notation "wp_pure" open_constr(efoc) :=
let e := eval simpl in e in
reshape_expr false e ltac:(fun K e' =>
unify e' efoc;
eapply (tac_wp_pure _ _ _ _ (fill K e'));
eapply (tac_wp_pure _ _ _ _ K e');
[iSolveTC (* PureExec *)
|try fast_done (* The pure condition for PureExec *)
|iSolveTC (* IntoLaters *)
......
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