

@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
