Commit bb37a795 authored by Ralf Jung's avatar Ralf Jung

fix build

parent d819164f
...@@ -66,18 +66,11 @@ Tactic Notation "wp_proj" := wp_pure (Fst _) || wp_pure (Snd _). ...@@ -66,18 +66,11 @@ Tactic Notation "wp_proj" := wp_pure (Fst _) || wp_pure (Snd _).
Tactic Notation "wp_case" := wp_pure (Case _ _ _). Tactic Notation "wp_case" := wp_pure (Case _ _ _).
Tactic Notation "wp_match" := wp_case; wp_let. Tactic Notation "wp_match" := wp_case; wp_let.
<<<<<<< HEAD Lemma tac_wp_bind `{heapG Σ} K Δ s E Φ e f :
Lemma tac_wp_bind `{heapG Σ} K Δ s E Φ e :
envs_entails Δ (WP e @ s; E {{ v, WP fill K (of_val v) @ s; E {{ Φ }} }})%I
envs_entails Δ (WP fill K e @ s; E {{ Φ }}).
Proof. rewrite /envs_entails=> ->. by apply: wp_bind. Qed.
=======
Lemma tac_wp_bind `{heapG Σ} K Δ E Φ e f :
f = (λ e, fill K e) (* as an eta expanded hypothesis so that we can `simpl` it *) f = (λ e, fill K e) (* as an eta expanded hypothesis so that we can `simpl` it *)
envs_entails Δ (WP e @ E {{ v, WP f (of_val v) @ E {{ Φ }} }})%I envs_entails Δ (WP e @ s; E {{ v, WP f (of_val v) @ s; E {{ Φ }} }})%I
envs_entails Δ (WP fill K e @ E {{ Φ }}). envs_entails Δ (WP fill K e @ s; E {{ Φ }}).
Proof. rewrite /envs_entails=> -> ->. by apply: wp_bind. Qed. Proof. rewrite /envs_entails=> -> ->. by apply: wp_bind. Qed.
>>>>>>> master
Ltac wp_bind_core K := Ltac wp_bind_core K :=
lazymatch eval hnf in K with lazymatch eval hnf in K with
......
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