BranchCommit messageAuthorAge
FPcompUpdate the proofs after rebaseXavier Leroy8 months
aarch64AArch64: wrong expected type for arguments of Cmaskl{zero,notzero}xavier.leroy3 months
conditional-moveIf-conversion optimization for CminorXavier Leroy6 months
floatofintux86 branchless implementation of float -> unsigned int32 conversionXavier Leroy6 months
masterAllow Coq 8.10.2.Bernhard Schommer6 days
no-pervasivesClarify "open" statementsXavier Leroy5 months
TagDownloadAuthorAge  CompCert-3.6.tar.gz  CompCert-3.6.tar.bz2  Xavier Leroy3 months  CompCert-3.5.tar.gz  CompCert-3.5.tar.bz2  Xavier Leroy9 months  CompCert-3.4.tar.gz  CompCert-3.4.tar.bz2  Xavier Leroy15 months  CompCert-3.3.tar.gz  CompCert-3.3.tar.bz2  Xavier Leroy18 months  CompCert-3.2.tar.gz  CompCert-3.2.tar.bz2  Bernhard Schommer23 months  CompCert-3.1.tar.gz  CompCert-3.1.tar.bz2  Xavier Leroy2 years  CompCert-3.0.1.tar.gz  CompCert-3.0.1.tar.bz2  Xavier Leroy3 years  CompCert-3.0.tar.gz  CompCert-3.0.tar.bz2  Xavier Leroy3 years  CompCert-2.7.1.tar.gz  CompCert-2.7.1.tar.bz2  Xavier Leroy3 years  CompCert-2.7.tar.gz  CompCert-2.7.tar.bz2  Xavier Leroy3 years
AgeCommit messageAuthor
6 daysAllow Coq 8.10.2.HEADmasterBernhard Schommer
11 daysFix for AArch64 alignment problem (#206)Bernhard Schommer
11 daysAdded dwarf register numbers for aarch64Bernhard Schommer
14 daysAdded back unused_ais_parameter warning.Bernhard Schommer
2019-11-25Simplified diagnostics module.Bernhard Schommer
2019-11-12Remove no longer needed file PrintLTLinBernhard Schommer
2019-11-12Use `intuition idtac` instead of `intuition` (#321)Vincent Laporte
2019-10-31Raise minimal required versions for OCaml and Coq (#203)Bernhard Schommer
2019-10-30More robust proof of `size_and` (#320)Frédéric Besson
2019-10-28Add support for Coq 8.10.1Xavier Leroy