|
|
|
@1280
|
9 years |
sacerdot |
Some progress in the porting of RTLAbstoRTL to the joint syntax:
1) …
|
|
|
|
@1270
|
9 years |
sacerdot |
Making RTL syntax an instance of Joint.
|
|
|
|
@1269
|
9 years |
sacerdot |
Useless include removed.
|
|
|
|
@1254
|
9 years |
sacerdot |
More progress towards porting of RTLtoERTL to joint syntax.
|
|
|
|
@1252
|
9 years |
sacerdot |
graph_params added to joint/Joint.ma, together with useful common …
|
|
|
|
@1248
|
9 years |
mulligan |
deleted files that do not compile in utilities, changed ertl.ma to use …
|
|
|
|
@1242
|
9 years |
sacerdot |
Some clean-up.
|
|
|
|
@1241
|
9 years |
mulligan |
changes for claudio
|
|
|
|
@1223
|
9 years |
mulligan |
changes
|
|
|
|
@1221
|
9 years |
sacerdot |
Cleanup.
|
|
|
|
@1220
|
9 years |
sacerdot |
ERTL ported to the new joint syntax.
|
|
|
|
@1183
|
9 years |
mulligan |
removed parameterised label types in the three lowest level languages
|
|
|
|
@1178
|
9 years |
mulligan |
fixed ertl.ma to use new version of joint params
|
|
|
|
@1175
|
9 years |
mulligan |
changes to ertl pass
|
|
|
|
@1171
|
9 years |
mulligan |
changes made on claudio's request: changed order of nesting in the …
|
|
|
|
@1168
|
9 years |
sacerdot |
Joint statements parameterized over a record.
|
|
|
|
@1165
|
9 years |
mulligan |
more changes
|
|
|
|
@1163
|
9 years |
mulligan |
even more streamlining and fixes to get things type checking
|
|
|
|
@1161
|
9 years |
mulligan |
changes from today: merged ertl, ltl and lin into one datatype to …
|
|
|
|
@1138
|
9 years |
mulligan |
merged ertl_st_opaccs_a and ertl_st_opaccs_b into each other
|
|
|
|
@1136
|
9 years |
mulligan |
fixed ertl pass
|
|
|
|
@1131
|
9 years |
mulligan |
changes to syntax of ertl: removed ertl_st_addr_l and ertl_st_addr_h …
|
|
|
|
@1107
|
9 years |
mulligan |
got rtl-ertl pass working again
|
|
|
|
@1084
|
9 years |
mulligan |
more added on ertl pass: not sure how much should be axiomatised wrt …
|
|
|
|
@1082
|
9 years |
mulligan |
work from today on ertl -> ltl pass
|
|
|
|
@1077
|
9 years |
mulligan |
ack, dependent types are scary
|
|
|
|
@1071
|
9 years |
mulligan |
changes the specific form that the added proofs take to use None, not …
|
|
|
|
@878
|
9 years |
campbell |
Removal of manually inserted record projections.
|
|
|
|
@783
|
9 years |
mulligan |
rtl to ertl pass complete (modulo some straightforward axioms that …
|
|
|
|
@782
|
9 years |
mulligan |
More work on rtl-ertl pass from today, plus resolved conflict.
|
|
|
|
@777
|
9 years |
mulligan |
Lots of work on RTL to ERTL pass from today.
|
|
|
|
@759
|
9 years |
mulligan |
More work on the RTL to ERTL pass.
|
|
|
|
@756
|
9 years |
mulligan |
Made a start on RTL. Renaming in ERTL and below to move closer to …
|
|
|
|
@753
|
9 years |
mulligan |
Work from today.
|
|
|
|
@745
|
9 years |
mulligan |
Changes from yesterday. Slowly implementing the functorized …
|
|
|
|
@735
|
9 years |
mulligan |
Changes from today
|
|
|
|
@733
|
9 years |
mulligan |
Fixed partial commit.
|
