Commit 95663185 authored by charguer's avatar charguer

fix compile

parent 97ff136d
......@@ -379,7 +379,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 *)
try solve [ hsimpl ]. (* --COMPATIBILITY V8.7 *)
xchange (MList_cons p). subst L2; rew_list. hsimpl. }
{ subst. xchanges MList_null_inv ;=> EL. subst L2; rew_list.
xvals~. }
......
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