|
|
|
@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
|
7 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
|
8 years |
sacerdot |
Bugs fixed: fresh_label changes the label universe, but this was not …
|
|
|
|
@1283
|
8 years |
sacerdot |
Bad programming practice removed: change_label is no longer required …
|
|
|
|
@1282
|
8 years |
sacerdot |
Cosmetic change: names of joint statements/instructions shortened and …
|
|
|
|
@1280
|
8 years |
sacerdot |
Some progress in the porting of RTLAbstoRTL to the joint syntax:
1) …
|
