

@3263

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



@3037

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



@2980

7 years 
tranquil 
fixed b_graph_translate



@2970

7 years 
tranquil 
now joint_if_entry can change when a preamble is added, so code points …



@2946

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



@2855

7 years 
piccolo 
little bug fixed in TranslateUtils?.



@2843

7 years 
piccolo 
1) Fixed a litte bug in Joint.ma
2) ERTL to ERTLptr correctness proof …



@2823

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



@2808

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



@2806

7 years 
tranquil 
new b_graph_translate obligations



@2723

7 years 
campbell 
Library name typo fixed.



@2716

7 years 
sacerdot 
utilities/deqsets.ma => utilities/deqsets_extra.ma for extraction



@2708

7 years 
tranquil 
fixed linearise and LINToASM
LINToASM has now correct transformation …



@2688

7 years 
tranquil 
* in Arithmeticcs.ma: commented include that breaks script in latest …



@2681

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



@2675

7 years 
tranquil 
* a generic graph program transformation



@2674

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



@2595

7 years 
tranquil 
* dropped locals and exit from definition of joint_if_function
* new …



@2557

7 years 
tranquil 
minor modification of commented (for now) proof of correctness of …



@2532

7 years 
tranquil 
added FCOND in LIN, and rewritten linearise so that it never adds a …



@2443

7 years 
tranquil 
changed joint's stack pointer and internal stack



@2286

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



@1995

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



@1599

8 years 
sacerdot 
Start of merging of stuff into the standard library of Matita.



@1521

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



@1516

8 years 
sacerdot 
Ported to syntax of Matita 0.99.1.



@1515

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



@1352

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



@1284

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



@1283

9 years 
sacerdot 
Bad programming practice removed: change_label is no longer required …



@1282

9 years 
sacerdot 
Cosmetic change: names of joint statements/instructions shortened and …



@1280

9 years 
sacerdot 
Some progress in the porting of RTLAbstoRTL to the joint syntax:
1) …
