| Commit message (Expand) | Author | Age | Files | Lines |
|---|
| * | More efficient implementations of map, fold, etc. | xleroy | 2014-08-27 | 1 | -164/+109 |
| * | The NaN behavior of float_of_single differs on PowerPC and on IA32/ARM. | xleroy | 2014-07-28 | 1 | -73/+18 |
| * | Merge of "newspilling" branch: | xleroy | 2014-07-23 | 3 | -1468/+2529 |
| * | Tweaks to support defunctorization. | xleroy | 2014-07-23 | 1 | -9/+19 |
| * | Add Proof keyword so that documentation generation works | jjourdan | 2014-07-04 | 1 | -0/+2 |
| * | Cleaner, more resilient parsing of pragmas. | xleroy | 2014-06-05 | 2 | -0/+78 |
| * | Integration of Jacques-Henri Jourdan's verified parser. | xleroy | 2014-04-29 | 1 | -0/+50 |
| * | Constprop: use "not" for "xorimm(-1)"; optimize == 1 and != 0 comparisons ove... | xleroy | 2014-04-09 | 1 | -0/+10 |
| * | Merge of branch linear-typing: | xleroy | 2014-04-06 | 1 | -66/+0 |
| * | floatoflong_from_words, floatoflongu_from_words : proof of PowerPc implementa... | jjourdan | 2014-03-13 | 1 | -89/+316 |
| * | floatoflong_decomp, floatoflongu_decomp | jjourdan | 2014-03-11 | 1 | -0/+238 |
| * | Silence the warning "Cannot build inversion information". | xleroy | 2014-02-24 | 1 | -9/+10 |
| * | Introduce and use the platform-specific Archi module giving: | xleroy | 2014-01-03 | 1 | -7/+6 |
| * | Merge of branch value-analysis. | xleroy | 2013-12-20 | 4 | -53/+615 |
| * | Axioms: remove prop_ext, currently unused AND unsound in Coq 8.4. | xleroy | 2013-12-15 | 1 | -23/+17 |
| * | Merge of the "alignas" branch. | xleroy | 2013-10-05 | 1 | -0/+55 |
| * | Slightly more efficient conversion positive <-> int | xleroy | 2013-09-26 | 1 | -17/+22 |
| * | Small improvements in compilation times for the register allocation pass. | xleroy | 2013-09-20 | 2 | -1/+60 |
| * | Floats.v, Nan.v: hard-wire the general shape of binop_pl, so that no axioms | xleroy | 2013-09-14 | 1 | -21/+119 |
| * | Simplify LPMap by smashing bottoms. | xleroy | 2013-08-12 | 1 | -138/+40 |
| * | Merge of Flocq version 2.2.0. | xleroy | 2013-08-02 | 1 | -105/+339 |
| * | Optimize integer divisions by positive constants, turning them into | xleroy | 2013-07-29 | 1 | -0/+28 |
| * | Add another expansion of shrx in terms of shifts and adds (from Hacker's Deli... | xleroy | 2013-07-28 | 1 | -42/+72 |
| * | More properties about subtraction and borrow. | xleroy | 2013-07-15 | 1 | -18/+59 |
| * | More accurate model of condition register flags for ARM and IA32. | xleroy | 2013-07-13 | 2 | -8/+125 |
| * | Revised handling of int->float conversions: | xleroy | 2013-07-08 | 1 | -3/+81 |
| * | Treat casts int64 -> float32 as primitive operations instead of two | xleroy | 2013-07-03 | 1 | -0/+18 |
| * | Update LICENSE file and headers for dual-licensed files. | xleroy | 2013-06-17 | 5 | -380/+14 |
| * | Merge of the "princeton" branch: | xleroy | 2013-06-16 | 1 | -0/+3 |
| * | Merge of the float32 branch: | xleroy | 2013-05-19 | 1 | -0/+28 |
| * | Coq-defined equality functions for Allocation. | xleroy | 2013-05-01 | 1 | -0/+7 |
| * | Expand 64-bit integer comparisons into 32-bit integer comparisons. | xleroy | 2013-04-29 | 1 | -35/+59 |
| * | Decomposing 64-bit "less than" comparisons. | xleroy | 2013-04-29 | 1 | -9/+70 |
| * | Big merge of the newregalloc-int64 branch. Lots of changes in two directions: | xleroy | 2013-04-20 | 8 | -408/+1321 |
| * | Assorted changes to reduce stack and heap requirements when compiling very bi... | xleroy | 2013-03-16 | 1 | -0/+48 |
| * | 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 |
| * | Useless Import | xleroy | 2013-03-10 | 1 | -1/+0 |
| * | Glasnost: making transparent a number of definitions that were opaque | xleroy | 2013-03-10 | 6 | -44/+64 |
| * | Assorted cleanups, esp. to avoid generating _rec and _rect recursors in | xleroy | 2013-03-09 | 6 | -164/+177 |
| * | Updated PowerPC port to new integers. | xleroy | 2013-02-12 | 1 | -1/+2 |
| * | 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 | 4 | -1381/+1655 |
| * | Some more properties. Refactored some proofs. | xleroy | 2013-02-04 | 1 | -21/+107 |
| * | Camlcoq.ml: bug in conversion Z to stringv1.12.1 | xleroy | 2013-01-29 | 1 | -3/+3 |
| * | Ported to Coq 8.4pl1. Merge of branches/coq-8.4. | xleroy | 2013-01-29 | 6 | -78/+215 |
| * | Remove some useless "Require". | xleroy | 2012-12-30 | 3 | -4/+0 |
| * | Merge of the clightgen branch: | xleroy | 2012-12-29 | 1 | -1/+3 |
| * | Integers: specialized function to compute x mod 2^N; used in "repr" to | xleroy | 2012-12-21 | 1 | -114/+177 |
| * | Flocq-based parsing of floating-point literals (Jacques-Henri Jourdan) | xleroy | 2012-11-03 | 1 | -3/+39 |
