aboutsummaryrefslogtreecommitdiffstats
BranchCommit messageAuthorAge
masterUpdate verilog back end with new x86 changesYann Herklotz13 months
dev/michalisMerge branch 'master' into dev/michalisYann Herklotz3 years
inl-cse-constAdd switch of passYann Herklotz3 years
aarch64AArch64: wrong expected type for arguments of Cmaskl{zero,notzero}xavier.leroy5 years
no-pervasivesClarify "open" statementsXavier Leroy5 years
floatofintux86 branchless implementation of float -> unsigned int32 conversionXavier Leroy5 years
conditional-moveIf-conversion optimization for CminorXavier Leroy5 years
FPcompUpdate the proofs after rebaseXavier Leroy5 years
 
TagDownloadAuthorAge
v3.10compcert-3.10.tar.gz  compcert-3.10.zip  Xavier Leroy3 years
v3.9compcert-3.9.tar.gz  compcert-3.9.zip  Xavier Leroy3 years
v3.8compcert-3.8.tar.gz  compcert-3.8.zip  Xavier Leroy4 years
v3.7compcert-3.7.tar.gz  compcert-3.7.zip  Xavier Leroy4 years
v3.6compcert-3.6.tar.gz  compcert-3.6.zip  Xavier Leroy5 years
v3.5compcert-3.5.tar.gz  compcert-3.5.zip  Xavier Leroy5 years
v3.4compcert-3.4.tar.gz  compcert-3.4.zip  Xavier Leroy6 years
v3.3compcert-3.3.tar.gz  compcert-3.3.zip  Xavier Leroy6 years
v3.2compcert-3.2.tar.gz  compcert-3.2.zip  Bernhard Schommer6 years
v3.1compcert-3.1.tar.gz  compcert-3.1.zip  Xavier Leroy7 years
[...]
 
AgeCommit messageAuthorFilesLines
2017-02-14Release 3.0.1 here we comev3.0.1Xavier Leroy2-1/+7
2017-02-13Give explicit scopes to notations a#b and a##b and a#b<-cXavier Leroy4-13/+21
2017-02-13Turn warning "deprecated-implicit-arguments" off while compiling FlocqXavier Leroy1-1/+4
2017-02-13Replace "Implicit Arguments" with "Arguments"Xavier Leroy8-19/+17
2017-02-13Use "Local" as prefixXavier Leroy22-38/+36
2017-02-13ARM, PowerPC: update Asmgenproof for Coq 8.6Xavier Leroy2-14/+21
2017-02-13Update Flocq to version 2.5.2Xavier Leroy8-132/+91
2017-02-13Merge branch 'coq-8.6' of https://github.com/maximedenes/CompCert into maxime...Xavier Leroy9-19/+22
2017-02-10Release 3.0 here we comev3.0Xavier Leroy2-2/+3
2017-02-10OS X: emit jumptables in .text segment, not .const segmentXavier Leroy1-1/+1
[...]
 
Clone
https://git.ymhg.org/compcert
ssh://git@git.ymhg.org:compcert
generated by cgit (git 2.34.1) at 2024-05-20 07:52:29 +0000