aboutsummaryrefslogtreecommitdiffstats
path: root/lib
Commit message (Expand)AuthorAgeFilesLines
* New parser based on new version of the Coq backend of Menhir (#276)Jacques-Henri Jourdan2019-07-051-51/+0
* Avoid relying on `Export` bug (#301)Maxime Dénès2019-07-041-1/+2
* More efficient test for powers of twoXavier Leroy2019-05-092-26/+105
* Rename Fappli_IEEE_extra.v into IEEE754_extra.vXavier Leroy2019-04-262-1/+1
* Move Z definitions out of Integers and into ZbitsXavier Leroy2019-04-263-839/+981
* lib/Coqlib.v: remove defns about multiplication, division, modulusXavier Leroy2019-04-233-101/+17
* Replace nat_of_Z with Z.to_natXavier Leroy2019-04-231-30/+7
* Floats.v: remove leftover Print commandsXavier Leroy2019-04-041-5/+1
* Floats.v: avoid using module Zlogarithm in the proofsXavier Leroy2019-04-031-10/+19
* Upgrade embedded version of Flocq to 3.1.Guillaume Melquiond2019-03-272-366/+371
* Integers.v: add modulus_gt_one (#259)Xavier Leroy2019-03-251-1/+7
* Minor simplifications in two proofs. (#280)Vincent Laporte2019-03-251-1/+1
* 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
generated by cgit (git 2.34.1) at 2024-06-02 22:13:07 +0000