| Commit message (Collapse) | Author | Age | Files | Lines | |
|---|---|---|---|---|---|
| * | fix bad reservation table for finvw | David Monniaux | 2022-02-12 | 1 | -2/+2 |
| | | |||||
| * | modulos | David Monniaux | 2022-02-11 | 4 | -1/+73 |
| | | |||||
| * | fp_modu32 | David Monniaux | 2022-02-11 | 1 | -1/+31 |
| | | |||||
| * | fp_modu64_correct | David Monniaux | 2022-02-11 | 1 | -0/+30 |
| | | |||||
| * | full2 mod correct | David Monniaux | 2022-02-11 | 1 | -0/+98 |
| | | |||||
| * | twostep_mod_longu_mostb_correct | David Monniaux | 2022-02-11 | 1 | -0/+94 |
| | | |||||
| * | moved stuff to appropriate places and removed irrelevant content | David Monniaux | 2022-02-11 | 2 | -258/+18 |
| | | |||||
| * | rm useless stuff | David Monniaux | 2022-02-11 | 1 | -123/+0 |
| | | |||||
| * | experiments in division | David Monniaux | 2022-02-11 | 2 | -0/+68 |
| | | |||||
| * | remove singleoflongu (does not exist) | David Monniaux | 2022-02-11 | 5 | -32/+73 |
| | | |||||
| * | rewrite with longu -> double -> single conversions | David Monniaux | 2022-02-11 | 1 | -23/+38 |
| | | |||||
| * | fp_divu64_correct | David Monniaux | 2022-02-10 | 1 | -0/+17 |
| | | |||||
| * | finished proof but still why need for decomposition | David Monniaux | 2022-02-10 | 1 | -16/+56 |
| | | |||||
| * | progress | David Monniaux | 2022-02-10 | 1 | -2/+44 |
| | | |||||
| * | progress | David Monniaux | 2022-02-10 | 1 | -23/+36 |
| | | |||||
| * | progress | David Monniaux | 2022-02-10 | 1 | -3/+15 |
| | | |||||
| * | Cgt / Clt | David Monniaux | 2022-02-10 | 1 | -7/+20 |
| | | |||||
| * | progress | David Monniaux | 2022-02-10 | 1 | -0/+18 |
| | | |||||
| * | progress | David Monniaux | 2022-02-10 | 1 | -2/+36 |
| | | |||||
| * | step1 expression is ok | David Monniaux | 2022-02-09 | 1 | -0/+36 |
| | | |||||
| * | full2_div_longu_correct | David Monniaux | 2022-02-09 | 1 | -0/+93 |
| | | |||||
| * | twostep_div_longu_mostb_correct | David Monniaux | 2022-02-09 | 1 | -11/+75 |
| | | |||||
| * | progress | David Monniaux | 2022-02-04 | 1 | -5/+10 |
| | | |||||
| * | progress | David Monniaux | 2022-02-04 | 1 | -2/+1 |
| | | |||||
| * | some progress | David Monniaux | 2022-02-04 | 1 | -0/+108 |
| | | |||||
| * | Merge ../kvx-work into kvx_fp_division | David Monniaux | 2022-02-03 | 6 | -12/+12 |
| |\ | |||||
| | * | Merge remote-tracking branch 'absint/master' into merge_absint | David Monniaux | 2022-02-02 | 6 | -12/+12 |
| | |\ | |||||
| | | * | Support Coq 8.15.0 | Xavier Leroy | 2022-01-31 | 1 | -2/+2 |
| | | | | |||||
| | | * | Adapt w.r.t. coq/coq#15442 (#425) | Pierre-Marie Pédrot | 2022-01-10 | 3 | -6/+6 |
| | | | | | | | | | | | | | | | | | | | | | | coq/coq#15442 changes the way `Program` names things, to make it uniform w.r.t. the standard naming schema. This commit removes dependencies on the names chosen by `Program`. Should be backwards compatible. Co-authored-by: Xavier Leroy <xavier.leroy@college-de-france.fr> | ||||
| | | * | Fix pattern for github-linguist. | Bernhard Schommer | 2021-12-14 | 1 | -2/+2 |
| | | | | |||||
| | | * | Enforce evaluation order in IRC.add_interf and IRC.add_pref | Xavier Leroy | 2021-12-07 | 1 | -2/+2 |
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | As written previously, OCaml can evaluate `nodeOfVar g v1` and `nodeOfVar g v2` in any order. Consequently, `v1` and `v2` can be entered in the `varTable` hash table in different order. This can result in different (but equally valid) register allocations. It's better to enforce one evaluation order for the sake of reproducible compilations when the OCaml version changes. | ||||
| * | | | fix path to coq image | David Monniaux | 2022-02-02 | 1 | -1/+1 |
| | | | | |||||
| * | | | update Coq | David Monniaux | 2022-02-02 | 1 | -3/+3 |
| | | | | |||||
| * | | | dependency to generate gappa script | David Monniaux | 2022-02-02 | 1 | -1/+1 |
| | | | | |||||
| * | | | attempts at dealing with gappa | David Monniaux | 2022-02-02 | 1 | -1/+8 |
| | | | | |||||
| * | | | full_div_longu_correct | David Monniaux | 2022-01-25 | 1 | -2/+28 |
| | | | | |||||
| * | | | some progress | David Monniaux | 2022-01-25 | 1 | -2/+66 |
| | | | | |||||
| * | | | attempt at definition | David Monniaux | 2022-01-25 | 1 | -0/+13 |
| | | | | |||||
| * | | | anystep_div_longu_correct | David Monniaux | 2022-01-25 | 1 | -0/+38 |
| | | | | |||||
| * | | | big progress on longu | David Monniaux | 2022-01-25 | 1 | -9/+61 |
| | | | | |||||
| * | | | some progress? | David Monniaux | 2022-01-25 | 1 | -126/+185 |
| | | | | |||||
| * | | | some progress | David Monniaux | 2022-01-24 | 1 | -2/+0 |
| | | | | |||||
| * | | | some progress | David Monniaux | 2022-01-24 | 1 | -19/+157 |
| | | | | |||||
| * | | | progress | David Monniaux | 2022-01-24 | 1 | -0/+121 |
| | | | | |||||
| * | | | rm spurious function | David Monniaux | 2022-01-24 | 1 | -115/+0 |
| | | | | |||||
| * | | | progress | David Monniaux | 2022-01-24 | 1 | -0/+190 |
| | | | | |||||
| * | | | twostep_div_longu_smallb_correct | David Monniaux | 2022-01-24 | 1 | -0/+82 |
| | | | | |||||
| * | | | done for small a | David Monniaux | 2022-01-24 | 1 | -3/+7 |
| | | | | |||||
| * | | | progress | David Monniaux | 2022-01-24 | 1 | -11/+31 |
| | | | | |||||
| * | | | progress | David Monniaux | 2022-01-24 | 1 | -7/+17 |
| | | | | |||||
 |
index : compcert-kvx | |
| Unnamed repository; edit this file 'description' to name the repository. |
| aboutsummaryrefslogtreecommitdiffstats |