summaryrefslogtreecommitdiff
path: root/checklink/Library.ml
Commit message (Expand)AuthorAge
* Update for single-precision floats. Calls to vararg functions remainGravatar xleroy2014-07-24
* Big merge of the newregalloc-int64 branch. Lots of changes in two directions:Gravatar xleroy2013-04-20
* Ported to Coq 8.4pl1. Merge of branches/coq-8.4.Gravatar xleroy2013-01-29
* checklink: configuration, indicate external symbolsGravatar varobert2012-07-12
* checklink: more stringent compilationGravatar varobert2012-07-11
* checklink: adaptation to the new floatsGravatar varobert2012-07-03
* checklink: Faster printingGravatar varobert2012-06-29
* checklink: improved user-friendlinessGravatar varobert2012-06-04
* checklink: improved error messagesGravatar varobert2012-06-01
* cchecklink continues when sections overlapGravatar varobert2012-05-24
* cchecklink now reads segments instead of sectionsGravatar varobert2012-05-10
* Added small data area support to checklinkGravatar varobert2012-04-20
* Faster ndxes_of_sym_nameGravatar varobert2012-04-12
* Added safety to potentially overflowing arithmeticsGravatar varobert2012-04-04
* Adjustments to cchecklink's options and verbosityGravatar varobert2012-04-04
* checklink: first import of Valentin Robert's validator for asm and linkGravatar xleroy2012-03-28