Changeset 1396


Ignore:
Timestamp:
Oct 17, 2011, 5:43:25 PM (8 years ago)
Author:
sacerdot
Message:

Proof obligation closed.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/RTL/semantics.ma

    r1390 r1396  
    8585      (set_m … mem
    8686       (set_sp … (mk_pointer XData b ? (mk_offset 0)) st)))).
    87 cases daemon (*CSC: XXXX easy lemma on alloc to be turned into a dependent type*)
     87cases b * #r #off #E >E %
    8888qed.
    8989
Note: See TracChangeset for help on using the changeset viewer.