Timeline
Jan 4, 2012:
- 7:42 PM Changeset [1634] by
- Update memory model examples syntax.
- 7:19 PM Changeset [1633] by
- Update Cminor pretty printer and examples.
Dec 20, 2011:
- 2:38 PM Changeset [1632] by
- - strengthened insert_lookup_opt
Dec 19, 2011:
- 2:48 PM Changeset [1631] by
- Use fact that type environments in Cminor have distinct variables to …
- 2:48 PM Changeset [1630] by
- Remainder of freshness in Clight to Cminor pass.
- 2:48 PM Changeset [1629] by
- Sort out most of the fresh names stuff in Clight to Cminor.
- 2:48 PM Changeset [1628] by
- Show that the universe generated by Clight/fresh.ma is good.
- 2:48 PM Changeset [1627] by
- Add some notions of freshness, and start using them for temporary …
- 2:48 PM Changeset [1626] by
- Add extra type safety in front end. NB: critical freshness parts …
Dec 16, 2011:
- 6:35 PM Changeset [1625] by
- before christmas
- 3:44 PM Changeset [1624] by
- commit for claudio
- 2:07 PM Changeset [1623] by
- strange matita issue
- 10:09 AM Changeset [1622] by
- to avoid conflicts, bug in typechecker?
Dec 15, 2011:
- 10:22 AM Changeset [1621] by
- to prevent conflicts
- 12:23 AM Changeset [1620] by
- One of the mutual cases of the open proof is practically finished.
- 12:02 AM Changeset [1619] by
- Major advancement.
Dec 14, 2011:
- 6:17 PM Changeset [1618] by
- Minor updates due to recent changes.
- 6:17 PM Changeset [1617] by
- Note stuff to do on structured traces.
- 5:57 PM Changeset [1616] by
- Partially ported to new Matita syntax. Because of some changes in …
- 5:28 PM Changeset [1615] by
- Policy now depends on Assembly and not the other way around.
- 5:00 PM Changeset [1614] by
- - split policy from assembly
- 4:41 PM Changeset [1613] by
- Coercion moved to Matita standard lib.
- 3:58 PM Changeset [1612] by
- All library ported to new Matita lib (finally).
- 3:35 PM Changeset [1611] by
- All of Cminor now compiles with the latest lib of Matita.
- 3:33 PM Changeset [1610] by
- Ported to new lib.
- 2:44 PM Changeset [1609] by
- - added alias to ASM/BitVectorTrie - removed double include from …
- 2:30 PM Changeset [1608] by
- Porting to new library still in progress.
- 1:50 PM Changeset [1607] by
- Porting to new library.
- 1:40 PM Changeset [1606] by
- Porting to last library of Matita.
- 1:18 PM Changeset [1605] by
- Porting to last standard library of Matita.
- 11:52 AM Changeset [1604] by
- for jaap
Dec 13, 2011:
- 5:37 PM Changeset [1603] by
- More proofs ported to new lib.
- 4:23 PM Changeset [1602] by
- giving up on fetch proofs for time being
- 2:49 PM Changeset [1601] by
- Files ported to new version of the standard library.
- 1:41 PM Changeset [1600] by
- utilities and ASM ported to the new standard library
- 1:34 AM Changeset [1599] by
- Start of merging of stuff into the standard library of Matita.
Dec 12, 2011:
- 5:53 PM Changeset [1598] by
- changes over the last couple of days
- 9:51 AM Changeset [1597] by
- fixed fetch for jaap
Dec 7, 2011:
- 4:24 PM Changeset [1596] by
- RTLabs structured traces: sort out passing of termination proofs around.
- 4:24 PM Changeset [1595] by
- We don't need an explicit termination count when building traces.
- 4:24 PM Changeset [1594] by
- Rework handling of termination information in RTLabs structured traces …
- 3:48 PM Changeset [1593] by
- - cleaned up Assembly, moved some definitions elsewhere
- 2:50 PM Changeset [1592] by
- - updated definitions to work with programs of maximum 216 instructions
Dec 6, 2011:
- 5:24 PM Changeset [1591] by
- work from today
- 5:13 PM Changeset [1590] by
- * got back to previous implementation of multiplication in RTLabs -> …
- 5:04 PM Changeset [1589] by
- * turned to argument-less return statements for RTLabs and RTL (there …
- 11:21 AM Changeset [1588] by
- All goals generated by Russell for execute_1* are now closed, mostly …
Dec 5, 2011:
- 5:16 PM Changeset [1587] by
- changes from today, including removing indexing of problematic …
- 1:11 PM Changeset [1586] by
- RTLabs structured traces: cost labels after jumps.
Note: See TracTimeline
for information about the timeline view.
