

@2946

7 years 
tranquil 
main novelties:
* there is an inbuilt stack_usage nat in joint …



@2931

8 years 
sacerdot 
Partial backtrack from Paolo's commit, that was partial.



@2925

8 years 
tranquil 
corrected bug in toggle_bool



@2918

8 years 
tranquil 
erased stupid accidental paste at the start of file (happened when …



@2917

8 years 
tranquil 
made it so that a 0 offset does not generate adding ops when accessing …



@2916

8 years 
tranquil 
corrected yet another endianness bug in load and store



@2915

8 years 
sacerdot 
Dead code removed.



@2912

8 years 
sacerdot 
Ouch, another bug in the very same function.
Fixed too, on an example …



@2911

8 years 
sacerdot 
Bug fixed in the translation of casts.



@2866

8 years 
tranquil 
corrected two bugs of the translation: constant translation used wrong …



@2823

8 years 
tranquil 
* corrected bug in ERTL semantics (both delframe and newframe did the …



@2808

8 years 
tranquil 
added local_stacksize to joint internal functions to accomodate for …



@2774

8 years 
sacerdot 
1. the compiler now outputs both the stack cost model and the max …



@2689

8 years 
tranquil 
* fixed passes up to linearisation



@2674

8 years 
tranquil 
* another change in block definition
* RTLabs > RTL and ERTL > …



@2640

8 years 
tranquil 
updated RTL and RTLabs to RTL translation



@2601

8 years 
sacerdot 
Extraction to ocaml is now working, with a couple of bugs left.
One …



@2505

8 years 
mckinna 
Cleaned up compiler.ma; some refactoring/additional code needed in …



@2493

8 years 
mckinna 
Change in cst_well_defd to fix previously broken defn of …



@2490

8 years 
tranquil 
switched back to Byte immediate (instead of beval ones)
propagated …



@2290

8 years 
campbell 
Remove jump tables from RTLabs > RTL.



@2286

8 years 
tranquil 
Big update!
* merge of all _paolo variants
* reorganised some depends …



@2176

8 years 
campbell 
Remove memory spaces other than XData and Code; simplify pointers as a …



@2103

8 years 
campbell 
Make transform_*program take a more general transformation to make …



@2032

8 years 
sacerdot 
!! BEWARE: major commit !!
1) [affects everybody]
split for …



@1995

8 years 
campbell 
Overall compiler definition; bits and pieces to
make everything happy(ish).



@1601

9 years 
sacerdot 
Files ported to new version of the standard library.



@1529

9 years 
campbell 
Update RTLabs to RTL with unary operation types.



@1521

9 years 
sacerdot 
Syntax change in Matita: change what where => change where what.



@1515

9 years 
campbell 
Add type of maps on positive binary numbers, and use them for …



@1408

9 years 
sacerdot 
1. Added joint/BEGlobalenvs that is a modification of …



@1358

9 years 
mulligan 
got rtlabs to rtl compiling, foldi_strong needs examining



@1356

9 years 
mulligan 
deleted redundant directory. added outlines for both reports, and …



@1354

9 years 
sacerdot 
One axiom closed.



@1352

9 years 
sacerdot 
This commit is made necessary by the last Matita change.
Inclusion is …



@1343

9 years 
mulligan 
fixed some bugs in the translation



@1331

9 years 
mulligan 
some changes, but i now have two contradictory proof obligations.



@1325

9 years 
mulligan 
finished implementing the translate constant function



@1315

9 years 
mulligan 
another move for the same reason. got rtlabs > rtl compiling again by …



@1314

9 years 
mulligan 
name changes so that bash tab completion actually works with some …


copied from src/RTLabs/RTLAbstoRTL.ma:



@1308

9 years 
mulligan 
changes to translate_cst
