|
|
|
@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
|
9 years |
campbell |
Remove jump tables from RTLabs -> RTL.
|
|
|
|
@2286
|
9 years |
tranquil |
Big update!
* merge of all _paolo variants
* reorganised some depends …
|
|
|
|
@2176
|
9 years |
campbell |
Remove memory spaces other than XData and Code; simplify pointers as a …
|
|
|
|
@2103
|
9 years |
campbell |
Make transform_*program take a more general transformation to make …
|
|
|
|
@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.
|
|
|
|
@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
|
10 years |
mulligan |
got rtlabs to rtl compiling, foldi_strong needs examining
|
|
|
|
@1356
|
10 years |
mulligan |
deleted redundant directory. added outlines for both reports, and …
|
|
|
|
@1354
|
10 years |
sacerdot |
One axiom closed.
|
|
|
|
@1352
|
10 years |
sacerdot |
This commit is made necessary by the last Matita change.
Inclusion is …
|
|
|
|
@1343
|
10 years |
mulligan |
fixed some bugs in the translation
|
|
|
|
@1331
|
10 years |
mulligan |
some changes, but i now have two contradictory proof obligations.
|
|
|
|
@1325
|
10 years |
mulligan |
finished implementing the translate constant function
|
|
|
|
@1315
|
10 years |
mulligan |
another move for the same reason. got rtlabs > rtl compiling again by …
|
|
|
|
@1314
|
10 years |
mulligan |
name changes so that bash tab completion actually works with some …
|
|
copied from src/RTLabs/RTLAbstoRTL.ma:
|
|
|
|
@1308
|
10 years |
mulligan |
changes to translate_cst
|
