| Commit message (Expand) | Author | Age | Files | Lines |
|---|
| * | 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 |
| * | Useless Import | xleroy | 2013-03-10 | 1 | -1/+0 |
| * | Glasnost: making transparent a number of definitions that were opaque | xleroy | 2013-03-10 | 29 | -120/+133 |
| * | Assorted cleanups, esp. to avoid generating _rec and _rect recursors in | xleroy | 2013-03-09 | 10 | -215/+260 |
| * | Improving the performance of exhaustive exploration (mode -all): | xleroy | 2013-03-09 | 1 | -18/+112 |
| * | Finished backtracking (cf previous commit) for ARM and PowerPC. | xleroy | 2013-03-04 | 7 | -815/+593 |
| * | Partial backtracking on previous commit: the "hole in Mach stack frame" | xleroy | 2013-03-03 | 7 | -857/+757 |
| * | Updates to follow recent changes in PrintAsm.ml | xleroy | 2013-03-01 | 1 | -14/+43 |
| * | Some builtins were renamed, updating | xleroy | 2013-03-01 | 1 | -4/+4 |
| * | Bug in Pbtbl | xleroy | 2013-03-01 | 1 | -1/+1 |
| * | No longer a dependency on Machtyping | xleroy | 2013-03-01 | 2 | -2/+1 |
| * | Fix 'interp' entry | xleroy | 2013-03-01 | 1 | -1/+1 |
| * | Testing dense switches | xleroy | 2013-03-01 | 3 | -1/+62 |
| * | Revised Stacking and Asmgen passes and Mach semantics: | xleroy | 2013-03-01 | 26 | -7039/+4809 |
| * | Updated ARM and PowerPC ports with new handling of __builtin_annot. | xleroy | 2013-02-24 | 9 | -90/+93 |
| * | Constant propagation within __builtin_annot. | xleroy | 2013-02-24 | 15 | -124/+250 |
| * | Pointers one past | xleroy | 2013-02-15 | 21 | -324/+565 |
| * | Updated PowerPC port to new integers. | xleroy | 2013-02-12 | 8 | -29/+59 |
| * | Be more like gcc in the way we display or not the usage message. | xleroy | 2013-02-12 | 1 | -8/+6 |
| * | Forgot theorem "sign_ext_narrow". | xleroy | 2013-02-12 | 1 | -0/+12 |
| * | lib/Integers.v: revised and extended, faster implementation based on | xleroy | 2013-02-10 | 11 | -1450/+1733 |
| * | Some more properties. Refactored some proofs. | xleroy | 2013-02-04 | 1 | -21/+107 |
| * | Typo in compare_mem causing merging of different states. | xleroy | 2013-02-02 | 1 | -1/+1 |
| * | Errors for excessively large global variables or stack frames. | xleroy | 2013-02-02 | 6 | -14/+17 |
| * | Camlcoq.ml: bug in conversion Z to stringv1.12.1 | xleroy | 2013-01-29 | 2 | -4/+4 |
| * | Ported to Coq 8.4pl1. Merge of branches/coq-8.4. | xleroy | 2013-01-29 | 69 | -1024/+1173 |
| * | Updated documentationv1.12 | xleroy | 2013-01-11 | 3 | -15/+15 |
| * | Update for release 1.12 | xleroy | 2013-01-09 | 4 | -9/+27 |
| * | Quote idents for safe re-parsing | xleroy | 2013-01-08 | 1 | -1/+1 |
