

@1330

9 years 
campbell 
Evict obsolete file.



@1321

9 years 
sacerdot 
No longer/never implemented files removed.



@1316

9 years 
campbell 
Merge in idlookupbranch to trunk.



@1296

9 years 
mulligan 
changes



@1285

9 years 
mulligan 
more implementation on maps, final push to get rtl abs to rtl working



@1274

9 years 
mulligan 
starting removing axioms from adts and giving them proper implementations



@1268

9 years 
sacerdot 
1) AST/Identifier.ma no longer used, utilities/IdentifierTools no …



@1266

9 years 
sacerdot 
Added second projection.



@1260

9 years 
mulligan 
commit for csc



@1250

9 years 
sacerdot 
1. Sigma types projections moved to utilities/extralib.ma
2. Extended …



@1248

9 years 
mulligan 
deleted files that do not compile in utilities, changed ertl.ma to use …



@1229

9 years 
mulligan 
changes



@1227

9 years 
mulligan 
changes



@1223

9 years 
mulligan 
changes



@1219

9 years 
mulligan 
a little more added



@1218

9 years 
mulligan 
a lot added to interference graph calculation



@1212

9 years 
mulligan 
more added on interference graphs



@1211

9 years 
mulligan 
fixed interference file



@1210

9 years 
mulligan 
getting rid of typeclasslike records in favour of filelevel axioms. …



@1209

9 years 
mulligan 
more work on int. graphs



@1208

9 years 
mulligan 
added adts for sets, tables and priority sets in order to make life …



@1196

9 years 
mulligan 
some more changes, need some additional datastructures



@1195

9 years 
campbell 
List find function.



@1193

9 years 
mulligan 
work on colouring algorithm halted as it can be axiomatised. now …



@1192

9 years 
mulligan 
some files that were missing / laying dormant on my computer



@1145

9 years 
mulligan 
changed naming in i8051 of classes of registers to make them consistent



@1127

9 years 
mulligan 
interference graphs axiomatised, more added to ertl



@1092

10 years 
campbell 
Some minor definitions for identifiers and lists.



@1075

10 years 
mulligan 
nearly completed rtl > ertl pass removing all option types with dep. types



@1066

10 years 
mulligan 
changes from today



@1052

10 years 
mulligan 
removed offsets after reading cerco mailing list



@1050

10 years 
mulligan 
adding dependent types to map datastructure to remove all option …



@1049

10 years 
mulligan 
more stuff added



@1048

10 years 
mulligan 
added implementation of haskell associative maps to clean up the mess …



@961

10 years 
campbell 
Use precise bitvector sizes throughout the front end, rather than …



@891

10 years 
campbell 
Revise proofs affected by recent matita change.



@882

10 years 
campbell 
Fix up fragile proofs for current version of matita.



@816

10 years 
campbell 
Clight to Cminor compilation, modulo switch statements, temporary …



@782

10 years 
mulligan 
More work on rtlertl pass from today, plus resolved conflict.



@780

10 years 
campbell 
Properly update set of registers that are used for pointers in Cminor …



@778

10 years 
mulligan 
moved register set into correct place



@766

10 years 
campbell 
Most of the Cminor to RTLabs stage.
Is buggy, generates inefficient …



@761

10 years 
campbell 
Enforce the use of declared identifiers/registers in Cminor/RTLabs.



@753

10 years 
mulligan 
Work from today.



@747

10 years 
campbell 
Merge the two AST files together (although some definitions still need …



@746

10 years 
mulligan 
Changes to bitvectortrieset: equality on sets. Added new file for …



@744

10 years 
campbell 
Evict Coqstyle integers from common/Integers.ma.
Make more bitvector …



@735

10 years 
mulligan 
Changes from today



@733

10 years 
mulligan 
Fixed partial commit.



@711

10 years 
sacerdot 
…



@709

10 years 
sacerdot 
Notations should NOT be redefined. Just add a new interpretation.



@699

10 years 
mulligan 
More or less finished formalisation of LIN.



@698

10 years 
mulligan 
Commit with changes to files to get our files to typecheck.



@697

10 years 
campbell 
Merge Clight branch of vectors and friends.
Start making stuff build.



@695

10 years 
campbell 
Rearrange Clight files a bit  will try to make them work again soon…



@691

10 years 
mulligan 
More movement of files within the repository.


copied from Deliverables/D4.24.3/utilities:



@491

10 years 
mulligan 
Initial commit of (part)formalisation of LIN intermediate language.
