source: src/CHANGES @ 723

Last change on this file since 723 was 723, checked in by mulligan, 10 years ago

Added dependent type internalising the invariant that LIN function bodies are non-empty and do not start with a label.

File size: 496 bytes
Line 
129/03/2011:
2  Label moved out of ASM.ma labelled_instruction datatype, as the Paris compiler
3  can only produce at most one label per instruction emitted.
4
5  Merged the LTL and LIN datatypes.
6
7  Added comments to the ASM datatypes.
8
9  Changed identifiers from bytes to words.
10
11  Formalised missing Assembly.ma file.
12
1330/03/2011:
14  Split translate_statements into two functions.
15
16  Added a dependent type for the invariant that a LIN function body does not
17  start with a label, and is not empty.
Note: See TracBrowser for help on using the repository browser.