| Commit message (Expand) | Author | Age | Files | Lines |
... | |
* | 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 |
* | Merge of branch seq-and-or. See Changelog for details. | xleroy | 2012-10-06 | 1 | -0/+14 |
* | Micro-optimization of (x & mask) >>s amount into a rolm when mask >= 0. | xleroy | 2012-07-09 | 1 | -0/+46 |
* | Process successors in increasing order. Helps preserving the nice CFG | xleroy | 2012-07-01 | 1 | -23/+62 |
* | Changelog: updated | xleroy | 2012-06-28 | 2 | -0/+54 |