Commit 4d335a51 authored by charguer's avatar charguer

compile 8.7

parent df884836
......@@ -378,6 +378,7 @@ Proof using.
xapps~. xif ;=> C.
{ xchanges~ (MList_not_null_inv_cons p) ;=> x p' L' EL.
xapps. xapp (>> M L1). xapps. xapps. { subst~. }
try hsimpl. (* --COMPATIBILITY V8.7 *)
xchange (MList_cons p). subst L2; rew_list. hsimpl. }
{ subst. xchanges MList_null_inv ;=> EL. subst L2; rew_list.
xvals~. }
......@@ -403,7 +404,7 @@ Proof using.
xapps~. xif ;=> C.
{ xchanges~ (MList_not_null_inv_cons p) ;=> x p' L' EL.
xapps. xapp (>> M L1 L'). { subst~. }
xapps. xapps. { subst~. } { subst; rew_list~. }
xapps. xapps (>> IH L' (L1&x)). { subst~. } { subst; rew_list~. }
xchange (MList_cons p). subst L2; rew_list. hsimpl. }
{ subst. xchanges MList_null_inv ;=> EL. subst L2; rew_list.
xvals~. }
......
......@@ -215,7 +215,7 @@ Proof using.
{ destruct P as (V&E&P).
applys Triple_enc_val_inv (fun r => \[r = enc V] \* H).
{ applys Rule_fun. rewrite E. hsimpl~. }
{ intros X. hpull ;=> EX. subst X. hchange P. hsimpl. simple~. } }
{ intros X. hpull ;=> EX. subst X. hchange P. hsimpl V. simple~. } }
{ destruct P as (V&E&P).
applys Triple_enc_val_inv (fun r => \[r = enc V] \* H).
{ applys Rule_fix. rewrite E. hsimpl~. }
......
......@@ -512,7 +512,7 @@ Lemma rule_consequence : forall t H' Q' H Q,
Proof using.
introv MH M MQ. intros HF h N.
forwards (h'&v&R&K): (rm M) HF h. { hhsimpl~. }
exists h' v. splits~. { hhsimpl. hchanges MQ. }
exists h' v. splits~. { hhsimpl. hchanges (MQ v). }
Qed.
Lemma rule_frame : forall t H Q H',
......
......@@ -597,7 +597,7 @@ Lemma rule_consequence : forall t H' Q' H Q,
Proof using.
introv MH M MQ. intros HF h N.
forwards (n&h'&v&R&K&C): (rm M) HF h. { hhsimpl~. }
exists n h' v. splits~. { hhsimpl. hchanges~ MQ. }
exists n h' v. splits~. { hhsimpl. hchanges~ (MQ v). }
Qed.
Lemma rule_frame : forall t H Q H',
......
......@@ -752,6 +752,7 @@ Ltac hcancel_cleanup tt :=
try hcancel_hint_remove tt;
try remove_empty_heaps_right tt;
try remove_empty_heaps_left tt;
try apply himpl_refl;
try apply hcancel_htop;
try apply hcancel_hempty_hstar_evar;
try apply hcancel_evar_hstar_hempty;
......
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