| Commit message (Expand) | Author | Age |
|---|
| * | More efficient implementations of map, fold, etc. |  xleroy | 2014-08-27 |
| * | The NaN behavior of float_of_single differs on PowerPC and on IA32/ARM. | xleroy | 2014-07-28 |
| * | Merge of "newspilling" branch: | xleroy | 2014-07-23 |
| * | Tweaks to support defunctorization. | xleroy | 2014-07-23 |
| * | Add Proof keyword so that documentation generation works |  jjourdan | 2014-07-04 |
| * | Cleaner, more resilient parsing of pragmas. | xleroy | 2014-06-05 |
| * | Integration of Jacques-Henri Jourdan's verified parser. | xleroy | 2014-04-29 |
| * | Constprop: use "not" for "xorimm(-1)"; optimize == 1 and != 0 comparisons ove... | xleroy | 2014-04-09 |
| * | Merge of branch linear-typing: | xleroy | 2014-04-06 |
| * | floatoflong_from_words, floatoflongu_from_words : proof of PowerPc implementa... | jjourdan | 2014-03-13 |
| * | floatoflong_decomp, floatoflongu_decomp | jjourdan | 2014-03-11 |
| * | Silence the warning "Cannot build inversion information". | xleroy | 2014-02-24 |
| * | Introduce and use the platform-specific Archi module giving: | xleroy | 2014-01-03 |
| * | Merge of branch value-analysis. | xleroy | 2013-12-20 |
| * | Axioms: remove prop_ext, currently unused AND unsound in Coq 8.4. | xleroy | 2013-12-15 |
| * | Merge of the "alignas" branch. | xleroy | 2013-10-05 |
| * | Slightly more efficient conversion positive <-> int | xleroy | 2013-09-26 |
| * | Small improvements in compilation times for the register allocation pass. | xleroy | 2013-09-20 |
| * | Floats.v, Nan.v: hard-wire the general shape of binop_pl, so that no axioms | xleroy | 2013-09-14 |
| * | Simplify LPMap by smashing bottoms. | xleroy | 2013-08-12 |
| * | Merge of Flocq version 2.2.0. | xleroy | 2013-08-02 |
| * | Optimize integer divisions by positive constants, turning them into | xleroy | 2013-07-29 |
| * | Add another expansion of shrx in terms of shifts and adds (from Hacker's Deli... | xleroy | 2013-07-28 |
| * | More properties about subtraction and borrow. | xleroy | 2013-07-15 |
| * | More accurate model of condition register flags for ARM and IA32. | xleroy | 2013-07-13 |
| * | Revised handling of int->float conversions: | xleroy | 2013-07-08 |
| * | Treat casts int64 -> float32 as primitive operations instead of two | xleroy | 2013-07-03 |
| * | Update LICENSE file and headers for dual-licensed files. | xleroy | 2013-06-17 |
| * | Merge of the "princeton" branch: | xleroy | 2013-06-16 |
| * | Merge of the float32 branch: | xleroy | 2013-05-19 |
| * | Coq-defined equality functions for Allocation. | xleroy | 2013-05-01 |
| * | Expand 64-bit integer comparisons into 32-bit integer comparisons. | xleroy | 2013-04-29 |
| * | Decomposing 64-bit "less than" comparisons. | xleroy | 2013-04-29 |
| * | Big merge of the newregalloc-int64 branch. Lots of changes in two directions: | xleroy | 2013-04-20 |
| * | Assorted changes to reduce stack and heap requirements when compiling very bi... | xleroy | 2013-03-16 |
| * | Bind some local defs with Let, makes extracted code cleaner | xleroy | 2013-03-12 |
| * | Maps: revised TREE interface; added mucho derived properties and operations i... | xleroy | 2013-03-12 |
| * | Useless Import | xleroy | 2013-03-10 |
| * | Glasnost: making transparent a number of definitions that were opaque | xleroy | 2013-03-10 |
| * | Assorted cleanups, esp. to avoid generating _rec and _rect recursors in | xleroy | 2013-03-09 |
| * | Updated PowerPC port to new integers. | xleroy | 2013-02-12 |
| * | Forgot theorem "sign_ext_narrow". | xleroy | 2013-02-12 |
| * | lib/Integers.v: revised and extended, faster implementation based on | xleroy | 2013-02-10 |
| * | Some more properties. Refactored some proofs. | xleroy | 2013-02-04 |
| * | Camlcoq.ml: bug in conversion Z to string | xleroy | 2013-01-29 |
| * | Ported to Coq 8.4pl1. Merge of branches/coq-8.4. | xleroy | 2013-01-29 |
| * | Remove some useless "Require". | xleroy | 2012-12-30 |
| * | Merge of the clightgen branch: | xleroy | 2012-12-29 |
| * | Integers: specialized function to compute x mod 2^N; used in "repr" to | xleroy | 2012-12-21 |
| * | Flocq-based parsing of floating-point literals (Jacques-Henri Jourdan) | xleroy | 2012-11-03 |
xleroy
jjourdan