summaryrefslogtreecommitdiff
path: root/pg
Commit message (Collapse)AuthorAge
* ia32/Select*: complete the modifications to shifts.Gravatar xleroy2014-04-11
| | | | | | | | | Makefile: missing "clean" actions. Makefile/pg/coq: honor $COQBIN if set (as suggested by P. Boutillier) to facilitate testing with different Coq versions. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2453 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Use "-as" to put CompCert modules in a compcert.xxx namespace.Gravatar xleroy2013-05-01
| | | | | | | | Simplified the scripts "coq" and "pg". Updated deps. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2228 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Use Flocq for floatsGravatar xleroy2012-06-28
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1939 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Merge of the nonstrict-ops branch:Gravatar xleroy2012-01-14
| | | | | | | | | | | - Most RTL operators now evaluate to Some Vundef instead of None when undefined behavior occurs. - More aggressive instruction selection. - "Bertotization" of pattern-matchings now implemented by a proper preprocessor. - Cast optimization moved to cfrontend/Cminorgen; removed backend/CastOptim. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1790 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Updated for Coq 8.3pl1. Some cleanups in test/*/Makefile.Gravatar xleroy2011-03-09
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1597 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e