| Commit message (Expand) | Author | Age | Files | Lines |
|---|
| * | Use "-as" to put CompCert modules in a compcert.xxx namespace. | xleroy | 2013-05-01 | 5 | -28/+50 |
| * | Oops, removed a crucial declaration for Allocation. | xleroy | 2013-05-01 | 1 | -0/+4 |
| * | Coq-defined equality functions for Allocation. (continued) | xleroy | 2013-05-01 | 2 | -6/+20 |
| * | Coq-defined equality functions for Allocation. | xleroy | 2013-05-01 | 6 | -45/+56 |
| * | Removing modules now unused | xleroy | 2013-05-01 | 6 | -2822/+0 |
| * | Add bswap16 | xleroy | 2013-04-30 | 1 | -1/+23 |
| * | Updated to Pbuiltin with list of results | xleroy | 2013-04-30 | 2 | -26/+26 |
| * | Updated to new CminorSel | xleroy | 2013-04-30 | 2 | -3/+3 |
| * | Typos in comments | xleroy | 2013-04-30 | 2 | -3/+3 |
| * | Updated | xleroy | 2013-04-30 | 1 | -3/+1 |
| * | Expand 64-bit integer comparisons into 32-bit integer comparisons. | xleroy | 2013-04-29 | 25 | -691/+590 |
| * | Decomposing 64-bit "less than" comparisons. | xleroy | 2013-04-29 | 1 | -9/+70 |
| * | Revert suppression of __builtin_{read,write}_reversed for x86 and ARM, | xleroy | 2013-04-29 | 12 | -37/+133 |
| * | Missing GLOB | xleroy | 2013-04-23 | 1 | -1/+1 |
| * | Make ia32/ code more portable across systems. | xleroy | 2013-04-23 | 29 | -879/+912 |
| * | driver: removed option -flonglong | xleroy | 2013-04-22 | 9 | -31/+282 |
| * | Results for ARM | xleroy | 2013-04-22 | 1 | -0/+4 |
| * | Labeled statements inside switch were incorrectly processed. | xleroy | 2013-04-22 | 1 | -0/+3 |
| * | Deactivate combination Aindexed 0 / Oadd, as it causes problems with chunk = ... | xleroy | 2013-04-21 | 2 | -4/+0 |
| * | Fixes in PowerPC port | xleroy | 2013-04-21 | 11 | -322/+392 |
| * | Add __builtin_bswap16 and __builtin_bswap32 to all ports. | xleroy | 2013-04-20 | 14 | -136/+128 |
| * | Rename arm/linux into arm/eabi, more descriptive. | xleroy | 2013-04-20 | 3 | -3/+4 |
| * | Split arch/int64.s into one file per function. | xleroy | 2013-04-20 | 45 | -1238/+2698 |
| * | Configuring the assembler used for the runtime lib | xleroy | 2013-04-20 | 3 | -2/+12 |
| * | Remove __i64_{neg,add,sub,mul}, now handled directly by the compiler. | xleroy | 2013-04-20 | 4 | -171/+0 |
| * | Added FFTW benchmark provided by Guillaume Melquiond | xleroy | 2013-04-20 | 3 | -2/+107 |
| * | Tests "floats" and "floats-basics" moved from test/c to test/regression | xleroy | 2013-04-20 | 7 | -21/+18 |
| * | Interp.ml: support printf of long long | xleroy | 2013-04-20 | 6 | -60/+4197 |
| * | Big merge of the newregalloc-int64 branch. Lots of changes in two directions: | xleroy | 2013-04-20 | 166 | -10626/+20598 |
| * | Updated issues with coqchk. See PR#3026 on the Coq bug tracker. | xleroy | 2013-04-14 | 1 | -6/+9 |
| * | List.iteri not in OCaml < 4.00, better not use it. | xleroy | 2013-04-08 | 1 | -2/+9 |
| * | Updated | xleroy | 2013-03-26 | 2 | -18/+23 |
| * | Error when calling un-prototyped function. | xleroy | 2013-03-25 | 1 | -6/+8 |
| * | Better locations for error messages relative to type specifiers. | xleroy | 2013-03-25 | 1 | -14/+9 |
| * | Watch out for behaviors exponential in the nesting of struct/union types. | xleroy | 2013-03-23 | 6 | -66/+78 |
| * | RTLtyping: now performed entirely in Coq, no need for an external Caml oracle... | xleroy | 2013-03-22 | 3 | -374/+713 |
| * | Update clightgen to changes in Camlcoq and in AST. | xleroy | 2013-03-20 | 2 | -15/+33 |
| * | Diab asm syntax issue | xleroy | 2013-03-20 | 1 | -1/+1 |
| * | For Pfreeframe, generate an "addi" over GPR1 when possible, to work around a ... | xleroy | 2013-03-18 | 2 | -3/+13 |
| * | Remove the C primitives for unsigned long long arithmetic, replaced | xleroy | 2013-03-18 | 4 | -53/+25 |
| * | More aggressive CSE across Ibuiltin. | xleroy | 2013-03-17 | 3 | -7/+36 |
| * | Assorted changes to reduce stack and heap requirements when compiling very bi... | xleroy | 2013-03-16 | 35 | -237/+534 |
| * | Machsem: no longer useful. | xleroy | 2013-03-14 | 1 | -259/+0 |
| * | Bind some local defs with Let, makes extracted code cleanerv1.13 | xleroy | 2013-03-12 | 1 | -2/+2 |
| * | Maps: revised TREE interface; added mucho derived properties and operations i... | xleroy | 2013-03-12 | 2 | -63/+256 |
| * | Suppress int64_unsigned_to_float, now unused. | xleroy | 2013-03-11 | 2 | -7/+0 |
| * | More updates for 1.13 | xleroy | 2013-03-11 | 1 | -2/+5 |
| * | Fixed parsing of hex float literals 0xNNNpMMM. | xleroy | 2013-03-11 | 5 | -4/+81 |
| * | Updated for version 1.13 | xleroy | 2013-03-11 | 2 | -11/+24 |
| * | Updating doc for 1.13 | xleroy | 2013-03-11 | 1 | -8/+5 |
