summaryrefslogtreecommitdiff
path: root/checklink/Asm_printers.ml
Commit message (Expand)AuthorAge
* Follow-up to commit 2613Gravatar xleroy2014-08-20
* PowerPC port: refactored the expansion of built-in functions andGravatar xleroy2014-07-28
* Update for single-precision floats. Calls to vararg functions remainGravatar xleroy2014-07-24
* Future-proofing: keep signature information in IA32 and PowerPC Asm, just lik...Gravatar xleroy2013-12-26
* powerpc/: new unary operation "addsymbol"Gravatar xleroy2013-11-17
* Update cchecklink w/ new Asm instructions Pmulh*Gravatar xleroy2013-07-29
* Updated to Pbuiltin with list of resultsGravatar xleroy2013-04-30
* 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
* Revert unintentional commit #1955Gravatar xleroy2012-07-06
* Ajout trunk CompCertGravatar blazy2012-07-04
* checklink: adaptation to the new floatsGravatar varobert2012-07-03
* Tracing each data chunk in debug modeGravatar varobert2012-04-04
* checklink: first import of Valentin Robert's validator for asm and linkGravatar xleroy2012-03-28
generated by cgit v1.2.3 (git 2.39.1) at 2024-04-29 20:09:30 +0000