aboutsummaryrefslogtreecommitdiffstats
path: root/coq
Commit message (Expand)AuthorAgeFilesLines
* No need for -R options, _CoqProject contains them alreadyXavier Leroy2020-09-211-4/+2
* Refine the type of function results in AST.signatureXavier Leroy2020-02-211-1/+1
* ia32/Select*: complete the modifications to shifts.xleroy2014-04-111-1/+1
* Use "-as" to put CompCert modules in a compcert.xxx namespace.xleroy2013-05-011-4/+2
* Use Flocq for floatsxleroy2012-06-281-1/+1
* Merge of the nonstrict-ops branch:xleroy2012-01-141-1/+1
* Merge of the newmem and newextcalls branches:xleroy2010-03-071-1/+11
* Reorganized the development, modularizing away machine-dependent parts.xleroy2008-12-301-1/+4
* Fusion des modifications faites sur les branches "tailcalls" et "smallstep".xleroy2007-08-041-1/+1
* Convenience commandxleroy2006-09-041-0/+4