Search:
Login
Preferences
Help/Guide
About Trac
Wiki
Timeline
Roadmap
Browse Source
View Tickets
Search
Context Navigation
View Latest Revision
source:
extracted
Revision Log Mode:
Stop on copy
Follow copies
Show only adds and deletes
View log starting at
and back to
Show at most
revisions per page.
Show full log messages
Legend:
Added
Modified
Copied or renamed
Diff
Rev
Age
Author
Log Message
(edit)
@2759
7 years
campbell
Print out costs, with choice of style. Note small anti-assertion patch …
(edit)
@2746
7 years
sacerdot
1. debugging code in glue 2. updated version
(edit)
@2743
7 years
sacerdot
Latest version of the compiler, extracted with the latest version of …
(edit)
@2742
7 years
sacerdot
Untrusted register colouring fully branched.
(edit)
@2740
7 years
sacerdot
Graph colouring terminated up to Uses that will be implemented in Matita.
(edit)
@2738
7 years
sacerdot
Porting the graph colouring stuff from the untrusted prototype to the …
(edit)
@2736
7 years
sacerdot
Untrusted fixpoint computation branched in.
(edit)
@2733
7 years
sacerdot
All axioms in set_adt implemented by hand.
(edit)
@2731
7 years
sacerdot
Minimal set of axioms implemented to make the driver run.
(edit)
@2730
7 years
sacerdot
Exported again.
(edit)
@2719
7 years
sacerdot
More values manually abstracted to functions to avoid failwiths at …
(edit)
@2718
7 years
sacerdot
set_empty turned from a value to a function because it is not …
(edit)
@2717
7 years
sacerdot
Extracted code for the whole compiler. The space cost model is not …
(edit)
@2649
7 years
sacerdot
…
(edit)
@2636
7 years
campbell
Extracted front-end.
(edit)
@2620
7 years
campbell
Sufficient hacking to run the extracted Clight semantics.
(edit)
@2602
7 years
piccolo
Dead code commented out.
(add)
@2601
7 years
sacerdot
Extraction to ocaml is now working, with a couple of bugs left. One …
Note:
See
TracRevisionLog
for help on using the revision log.
Download in other formats:
RSS Feed
ChangeLog