aboutsummaryrefslogtreecommitdiffstats
path: root/lib
Commit message (Expand)AuthorAgeFilesLines
* Make the checker happy (#272)Vincent Laporte2019-02-121-8/+8
* Add functions "ordered" and "compare" to Float and Float32Xavier Leroy2018-12-201-9/+20
* Import prim token notations before using themJason Gross2018-08-271-0/+1
* Various improvements in the wording of diagnostics.Michael Schmidt2018-08-021-3/+3
* Compatibility with OCaml 4.07 (#241)Xavier Leroy2018-07-101-1/+1
* Removed deprecated lemma.Bernhard Schommer2018-03-121-1/+1
* Resynchronize the LICENSE file and the license headers in individual files (#45)Xavier Leroy2018-01-056-251/+15
* Test for inline. Bug 22642Bernhard Schommer2017-12-081-1/+1
* Added simple div_one Theorem variants.Bernhard Schommer2017-12-011-0/+6
* New json printing interface.Bernhard Schommer2017-11-143-1/+190
* Merge pull request #191 from sigurdschneider/masterXavier Leroy2017-10-203-2/+3
|\
| * Ensure FunInd or Recdef is imported if functional induction is usedSigurd Schneider2017-07-203-2/+3
* | Remove coq warnings (#28)Bernhard Schommer2017-09-2211-182/+182
* | Some lemmas.Bernhard Schommer2017-09-211-0/+14
|/
* Formatted json printing.Bernhard Schommer2017-06-281-22/+32
* Hybrid 64bit/32bit PowerPC portBernhard Schommer2017-05-035-70/+230
* RISC-V port and assorted changesXavier Leroy2017-04-282-3/+25
* Adapt proofs to future handling of literal constants in Coq.Guillaume Melquiond2017-03-081-5/+2
* Replace "Implicit Arguments" with "Arguments"Xavier Leroy2017-02-132-6/+4
* Use "Local" as prefixXavier Leroy2017-02-131-1/+1
* Replace 'decide equality' in x86/Op.v by custom tactics from lib/BoolEqual.vXavier Leroy2016-12-261-0/+167
* C2C: revise typing and translation of __builtin_memcpy_alignedXavier Leroy2016-11-171-0/+6
* Finish the proofs of SelectLong for IA32Xavier Leroy2016-10-021-1/+108
* Improve code generation for 64-bit signed integer divisionXavier Leroy2016-10-021-0/+37
* Support for 64-bit architectures: generic supportXavier Leroy2016-10-011-3/+454
* IA32: model integer division and modulus closer to the machineXavier Leroy2016-09-181-0/+92
* Enrich Decidableplus and use it to simplify Cexec.do_ef_memcpyXavier Leroy2016-09-171-0/+28
* Decidableplus: remove stuff that was cut-and-paste from Coq 8.5 libraryXavier Leroy2016-09-171-48/+1
* Removed some implict arguments.Bernhard Schommer2016-09-051-5/+3
* Moved quoting functions in ResponsefileBernhard Schommer2016-08-162-2/+36
* Added simplified reader and printer for gnu @filesBernhard Schommer2016-07-203-134/+98
* Added heuristic for passing arg via responsefiles.Bernhard Schommer2016-07-122-20/+0
* Really added the function. Bug 18308Bernhard Schommer2016-07-112-3/+19
* Added function to write responsefiles.Bernhard Schommer2016-07-111-0/+24
* Merge branch 'master' into add-fileBernhard Schommer2016-07-1110-173/+156
|\
| * Port to Coq 8.5pl2Xavier Leroy2016-07-0810-173/+156
* | Added responsefile support for commandline.Bernhard Schommer2016-07-081-0/+133
|/
* Remove code that will is deprecated in ocaml 4.03Bernhard Schommer2016-06-211-0/+10
* ValueAnalysis: use ZTrees instead of ZMaps for abstracting contents of memory...Xavier Leroy2016-05-071-0/+80
* Revise the Stacking pass and its proof to make it easier to adapt to 64-bit a...Xavier Leroy2016-04-271-0/+244
* Merge pull request #92 from AbsInt/cleanupXavier Leroy2016-03-214-8/+18
|\
| * Merge branch 'master' into cleanupBernhard Schommer2016-03-212-34/+189
| |\
| * | Cleanup of AsmToJSON.Bernhard Schommer2016-03-161-2/+10
| * | Upgrade ocaml version needed and enable more warnings.Bernhard Schommer2016-03-102-6/+6
| * | Code cleanup.Bernhard Schommer2016-03-101-0/+2
* | | Also ignore windows line endings.Bernhard Schommer2016-03-211-1/+2
| |/ |/|
* | Preliminaries: extend the Coqlib and Maps libraries.Xavier Leroy2016-03-062-34/+189
|/
* Added printer for Configuration and finished Clflags.Bernhard Schommer2016-01-251-0/+9
* Started implementing a printer for Clflags.Bernhard Schommer2016-01-251-0/+33
* Open files in binary mode.Bernhard Schommer2015-11-301-2/+1
generated by cgit (git 2.34.1) at 2024-06-01 10:54:44 +0000