Changeset 1388 for src/CHANGES


Ignore:
Timestamp:
Oct 17, 2011, 10:54:50 AM (8 years ago)
Author:
sacerdot
Message:

fetch_result implemented for ERTL. This required a different istantiation of
resultT that is not in line with the OCaml's code. Look at CHANGES for details.
RTLToERTL has been ported in an hopefully correct manner.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/CHANGES

    r1198 r1388  
    8282  it only needs to do a simple pattern match per recursion and copes with deeper
    8383  arithmetic expressions such as (char)((int)x + (int)y + (int)z).
     84
     8517/10/2011: (CSC)
     86  In OCaml, RTL's and ERTL's St_return statement holds the return register list,
     87  to be used in is_final. In Matita, they don't. For RTL the information was
     88  duplicated in the internal function record. I have done the same for ERTL too.
     89  To be double checked with the OCaml semantics.
Note: See TracChangeset for help on using the changeset viewer.