aboutsummaryrefslogtreecommitdiffstats
path: root/lib
Commit message (Expand)AuthorAgeFilesLines
* Update LICENSE file and headers for dual-licensed files.xleroy2013-06-175-380/+14
* Merge of the "princeton" branch:xleroy2013-06-161-0/+3
* Merge of the float32 branch: xleroy2013-05-191-0/+28
* Coq-defined equality functions for Allocation.xleroy2013-05-011-0/+7
* Expand 64-bit integer comparisons into 32-bit integer comparisons.xleroy2013-04-291-35/+59
* Decomposing 64-bit "less than" comparisons.xleroy2013-04-291-9/+70
* Big merge of the newregalloc-int64 branch. Lots of changes in two directions:xleroy2013-04-208-408/+1321
* Assorted changes to reduce stack and heap requirements when compiling very bi...xleroy2013-03-161-0/+48
* Bind some local defs with Let, makes extracted code cleanerv1.13xleroy2013-03-121-2/+2
* Maps: revised TREE interface; added mucho derived properties and operations i...xleroy2013-03-122-63/+256
* Useless Importxleroy2013-03-101-1/+0
* Glasnost: making transparent a number of definitions that were opaquexleroy2013-03-106-44/+64
* Assorted cleanups, esp. to avoid generating _rec and _rect recursors in xleroy2013-03-096-164/+177
* Updated PowerPC port to new integers.xleroy2013-02-121-1/+2
* Forgot theorem "sign_ext_narrow".xleroy2013-02-121-0/+12
* lib/Integers.v: revised and extended, faster implementation based onxleroy2013-02-104-1381/+1655
* Some more properties. Refactored some proofs.xleroy2013-02-041-21/+107
* Camlcoq.ml: bug in conversion Z to stringv1.12.1xleroy2013-01-291-3/+3
* Ported to Coq 8.4pl1. Merge of branches/coq-8.4.xleroy2013-01-296-78/+215
* Remove some useless "Require".xleroy2012-12-303-4/+0
* Merge of the clightgen branch:xleroy2012-12-291-1/+3
* Integers: specialized function to compute x mod 2^N; used in "repr" toxleroy2012-12-211-114/+177
* Flocq-based parsing of floating-point literals (Jacques-Henri Jourdan)xleroy2012-11-031-3/+39
* Merge of branch seq-and-or. See Changelog for details.xleroy2012-10-061-0/+14
* Micro-optimization of (x & mask) >>s amount into a rolm when mask >= 0.xleroy2012-07-091-0/+46
* Process successors in increasing order. Helps preserving the nice CFGxleroy2012-07-011-23/+62
* Changelog: updatedxleroy2012-06-282-0/+54
* Use Flocq for floatsxleroy2012-06-283-103/+733
* More properties on mul/div/modxleroy2012-06-091-0/+39
* Memdata: cleanup continuedxleroy2012-05-261-0/+26
* Merge of the newmem branch:xleroy2012-05-215-96/+583
* More aggressive common subexpression elimination (CSE) of memory loads.xleroy2012-02-231-0/+50
* Merge of the nonstrict-ops branch:xleroy2012-01-141-20/+127
* Extraction: map Coq pairs to Caml pairs and Coq chars (type ascii) to Caml charsxleroy2011-10-181-20/+4
* Changelog, doc: updated for release 1.9v1.9xleroy2011-08-221-8/+7
* Cleaned up old commented-out partsxleroy2011-08-191-5/+0
* Merge of branch new-semantics: revised and strengthened top-level statements ...xleroy2011-07-151-0/+43
* Back from Oregon commit. xleroy2011-07-052-0/+24
* Relating neg and notxleroy2011-06-221-5/+42
* Merge of branch "unsigned-offsets":xleroy2011-04-091-23/+139
* Updated for Coq 8.3pl1. Some cleanups in test/*/Makefile.xleroy2011-03-094-23/+16
* float->int conversions, continued: weaker axiomatization.xleroy2010-10-291-22/+3
* Float.intoffloat and Float.intuoffloat are now partial functions.xleroy2010-10-282-8/+31
* Various algorithmic improvements that reduce compile times (thanks Alexandre ...xleroy2010-10-273-72/+905
* License for Floataux.mlxleroy2010-10-271-0/+3
* Merge of the reuse-temps branch:xleroy2010-09-021-17/+101
* Integers: cleaned up bitwise operations, redefined shr, zero_ext and sign_extxleroy2010-08-211-1024/+1009
* Support for inlined built-ins.xleroy2010-06-291-13/+45
* All axioms used in the CompCert developmentxleroy2010-06-281-0/+27
* Merging the Princeton implementation of the memory model. Separate axioms in...xleroy2010-06-284-5/+11
generated by cgit (git 2.34.1) at 2024-06-02 19:51:43 +0000