Commit c54446ca authored by Léon Gondelman 's avatar Léon Gondelman

get rid of Closed in Invoke

parent 0bc5d071
......@@ -551,12 +551,12 @@ Global Instance into_dcexpr_par E e1 e2 de1 de2:
IntoDCExpr E (e1 ||| e2) (dCPar de1 de2).
Proof. intros [-> ?] [-> ?]; split; simpl; auto. Qed.
Global Instance into_dcexpr_invoke E `{Closed [] e1} ef f `{!IntoVal ef f} de1 :
Global Instance into_dcexpr_invoke e1 E ef f `{!IntoVal ef f} de1 :
IntoDCExpr E e1 de1
IntoDCExpr E (call (ef, e1)) (dCInvoke f de1).
Proof.
intros. unfold IntoVal in *. simplify_eq /=.
split; simpl; auto; f_equal; by inversion H0.
intros HC. unfold IntoVal in *. simplify_eq /=.
split; simpl; auto; f_equal; apply HC.
Qed.
Global Instance into_dcexpr_unknown E e `{Closed [] e}:
......
......@@ -270,15 +270,8 @@ Section vcg.
| None => vcg_wp_awp_continuation R E de m Φ
end
| dCBind x de1 de2, S p =>
match vcg_sp' E m de1 with
| Some (m', mNew, dv1) =>
vcg_wp E m' (dce_subst x dv1 de2) R (λ E m'' dv2,
vcg_wp_bind E dv2 (denv_merge mNew m'') Φ) p
| None =>
vcg_wp E m de1 R (λ E m' dv1,
vcg_wp E m' (dce_subst x dv1 de2) R (λ E m'' dv2,
vcg_wp_bind E dv2 m'' Φ) p) p
end
vcg_wp E m de1 R (λ E m' dv1,
vcg_wp E m' (dce_subst x dv1 de2) R Φ p) p
| dCAlloc de1 de2, S p =>
match vcg_sp' E m de1 with
| Some (m', mNew, dv1) =>
......
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