aboutsummaryrefslogtreecommitdiffstats
Commit message (Expand)AuthorAgeFilesLines
* enlarge rangeHEADmasterDavid Monniaux2022-03-091-1/+1
* Merge remote-tracking branch 'origin/kvx_fp_division' into kvx-workDavid Monniaux2022-03-0731-20/+4784
|\
| * installationDavid Monniaux2022-03-071-2/+14
| * builtins pour signed div/modDavid Monniaux2022-02-164-0/+144
| * simpler modDavid Monniaux2022-02-162-8/+64
| * mods 64David Monniaux2022-02-151-0/+235
| * fp_divs32_correctDavid Monniaux2022-02-151-0/+41
| * int_mods_moduDavid Monniaux2022-02-151-0/+58
| * fp_divs32_correctDavid Monniaux2022-02-141-0/+137
| * Merge remote-tracking branch 'origin/kvx-bits' into kvx_fp_divisionDavid Monniaux2022-02-1417-18/+374
| |\
| * \ Merge remote-tracking branch 'origin/kvx-work' into kvx_fp_divisionDavid Monniaux2022-02-124-18/+79
| |\ \
| * | | fix bad reservation table for finvwDavid Monniaux2022-02-121-2/+2
| * | | modulosDavid Monniaux2022-02-114-1/+73
| * | | fp_modu32David Monniaux2022-02-111-1/+31
| * | | fp_modu64_correctDavid Monniaux2022-02-111-0/+30
| * | | full2 mod correctDavid Monniaux2022-02-111-0/+98
| * | | twostep_mod_longu_mostb_correctDavid Monniaux2022-02-111-0/+94
| * | | moved stuff to appropriate places and removed irrelevant contentDavid Monniaux2022-02-112-258/+18
| * | | rm useless stuffDavid Monniaux2022-02-111-123/+0
| * | | experiments in divisionDavid Monniaux2022-02-112-0/+68
| * | | remove singleoflongu (does not exist)David Monniaux2022-02-115-32/+73
| * | | rewrite with longu -> double -> single conversionsDavid Monniaux2022-02-111-23/+38
| * | | fp_divu64_correctDavid Monniaux2022-02-101-0/+17
| * | | finished proof but still why need for decompositionDavid Monniaux2022-02-101-16/+56
| * | | progressDavid Monniaux2022-02-101-2/+44
| * | | progressDavid Monniaux2022-02-101-23/+36
| * | | progressDavid Monniaux2022-02-101-3/+15
| * | | Cgt / CltDavid Monniaux2022-02-101-7/+20
| * | | progressDavid Monniaux2022-02-101-0/+18
| * | | progressDavid Monniaux2022-02-101-2/+36
| * | | step1 expression is okDavid Monniaux2022-02-091-0/+36
| * | | full2_div_longu_correctDavid Monniaux2022-02-091-0/+93
| * | | twostep_div_longu_mostb_correctDavid Monniaux2022-02-091-11/+75
| * | | progressDavid Monniaux2022-02-041-5/+10
| * | | progressDavid Monniaux2022-02-041-2/+1
| * | | some progressDavid Monniaux2022-02-041-0/+108
| * | | Merge ../kvx-work into kvx_fp_divisionDavid Monniaux2022-02-036-12/+12
| |\ \ \
| * | | | fix path to coq imageDavid Monniaux2022-02-021-1/+1
| * | | | update CoqDavid Monniaux2022-02-021-3/+3
| * | | | dependency to generate gappa scriptDavid Monniaux2022-02-021-1/+1
| * | | | attempts at dealing with gappaDavid Monniaux2022-02-021-1/+8
| * | | | full_div_longu_correctDavid Monniaux2022-01-251-2/+28
| * | | | some progressDavid Monniaux2022-01-251-2/+66
| * | | | attempt at definitionDavid Monniaux2022-01-251-0/+13
| * | | | anystep_div_longu_correctDavid Monniaux2022-01-251-0/+38
| * | | | big progress on longuDavid Monniaux2022-01-251-9/+61
| * | | | some progress?David Monniaux2022-01-251-126/+185
| * | | | some progressDavid Monniaux2022-01-241-2/+0
| * | | | some progressDavid Monniaux2022-01-241-19/+157
| * | | | progressDavid Monniaux2022-01-241-0/+121