

@1624

9 years 
mulligan 
commit for claudio



@1623

9 years 
mulligan 
strange matita issue



@1622

9 years 
mulligan 
to avoid conflicts, bug in typechecker?



@1621

9 years 
mulligan 
to prevent conflicts



@1620

9 years 
sacerdot 
One of the mutual cases of the open proof is practically finished.



@1619

9 years 
sacerdot 
Major advancement.



@1618

9 years 
campbell 
Minor updates due to recent changes.



@1617

9 years 
campbell 
Note stuff to do on structured traces.



@1616

9 years 
sacerdot 
Partially ported to new Matita syntax.
Because of some changes in …



@1615

9 years 
sacerdot 
Policy now depends on Assembly and not the other way around.



@1614

9 years 
boender 
 split policy from assembly



@1613

9 years 
sacerdot 
Coercion moved to Matita standard lib.



@1612

9 years 
sacerdot 
All library ported to new Matita lib (finally).



@1611

9 years 
sacerdot 
All of Cminor now compiles with the latest lib of Matita.



@1610

9 years 
sacerdot 
Ported to new lib.



@1609

9 years 
boender 
 added alias to ASM/BitVectorTrie
 removed double include from …



@1608

9 years 
sacerdot 
Porting to new library still in progress.



@1607

9 years 
sacerdot 
Porting to new library.



@1606

9 years 
sacerdot 
Porting to last library of Matita.



@1605

9 years 
sacerdot 
Porting to last standard library of Matita.



@1604

9 years 
mulligan 
for jaap



@1603

9 years 
sacerdot 
More proofs ported to new lib.



@1602

9 years 
mulligan 
giving up on fetch proofs for time being



@1601

9 years 
sacerdot 
Files ported to new version of the standard library.



@1600

9 years 
sacerdot 
utilities and ASM ported to the new standard library



@1599

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



@1598

9 years 
mulligan 
changes over the last couple of days



@1597

9 years 
mulligan 
fixed fetch for jaap



@1596

9 years 
campbell 
RTLabs structured traces: sort out passing of termination proofs around.



@1595

9 years 
campbell 
We don't need an explicit termination count when building traces.



@1594

9 years 
campbell 
Rework handling of termination information in RTLabs structured traces …



@1593

9 years 
boender 
 cleaned up Assembly, moved some definitions elsewhere



@1592

9 years 
boender 
 updated definitions to work with programs of maximum 2^{16 instructions}



@1591

9 years 
mulligan 
work from today


