

@3263

8 years 
tranquil 
moved callee saved saving and restoring to ERTL > LTL pass (untrusted …



@3256

8 years 
tranquil 
fixed compilation



@3255

8 years 
tranquil 
* dropped newframe and delframe (to be integrated in calls and returns …



@3145

8 years 
tranquil 
* removed sigma types from traces of intensional events
* completed …



@3037

8 years 
tranquil 
* ADDRESS joint instruction now has also an offset
* corrected call to …



@2876

8 years 
tranquil 
corrected another endianess bug in joint_semantics. Switched some …



@2862

8 years 
sacerdot 
Repaired, a reverse was enough.



@2861

8 years 
mckinna 
PROVISIONAL commit:
Unintentional list reversal cause final step of …



@2806

8 years 
tranquil 
new b_graph_translate obligations



@2689

8 years 
tranquil 
* fixed passes up to linearisation



@2681

8 years 
tranquil 
* improvements to the graph translation function
* fixed passes up to LTL



@2659

8 years 
sacerdot 
Tailcall elimination no longer necessary:
1. the backend is almost …



@2490

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



@2286

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



@2103

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



@2035

9 years 
sacerdot 
Fixed



@2032

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



@1995

9 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.



@1516

9 years 
sacerdot 
Ported to syntax of Matita 0.99.1.



@1481

9 years 
sacerdot 
Proof fixed. The new standard library does not index any longer the …



@1450

9 years 
sacerdot 
Disambiguation problem avoided.



@1388

9 years 
sacerdot 
fetch_result implemented for ERTL. This required a different …



@1352

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



@1322

9 years 
sacerdot 
address => stack_address



@1315

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


copied from src/RTL/RTLtoERTL.ma:



@1284

9 years 
sacerdot 
Bugs fixed: fresh_label changes the label universe, but this was not …
