aboutsummaryrefslogtreecommitdiffstats
path: root/lib
Commit message (Expand)AuthorAgeFilesLines
...
* | | | gremove_tDavid Monniaux2020-02-041-0/+36
* | | | gcombine_nullDavid Monniaux2020-02-041-0/+13
* | | | gcombine_nullDavid Monniaux2020-02-041-1/+39
|/ / /
* | | Use `intuition idtac` instead of `intuition` (#321)Vincent Laporte2019-11-121-1/+1
* | | More robust proof of `size_and` (#320)Frédéric Besson2019-10-301-4/+5
* | | Make explicit the use of hints from OrderedType (#316)Vincent Laporte2019-10-022-7/+9
| |/ |/|
* | AArch64 portXavier Leroy2019-08-081-24/+136
* | More lemmas about powers of 2Xavier Leroy2019-08-071-0/+14
* | Added Int.same_if_eqXavier Leroy2019-08-071-0/+5
* | Properties of combinations of shifts and zero-/sign-extensionXavier Leroy2019-08-071-0/+249
* | Define integer sign extension for zero bitsXavier Leroy2019-08-072-42/+57
* | Zbits.v: add bit extraction and bit insertionXavier Leroy2019-08-071-0/+57
* | Coq 8.10 compatibility: tweak Argument commandXavier Leroy2019-08-071-1/+1
* | Coq 8.10 compatibility: make explicit the "core" hint databaseXavier Leroy2019-08-071-2/+2
|/
* Another way to derive floatofintu from floatofintXavier Leroy2019-07-171-0/+41
* Add floating-point square root and fused multiply-addXavier Leroy2019-07-171-3/+51
* Revised specification of NaN payload behaviorXavier Leroy2019-07-121-124/+104
* 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
generated by cgit (git 2.34.1) at 2024-05-20 09:59:09 +0000