| Commit message (Collapse) | Author | Age | Files | Lines | |
|---|---|---|---|---|---|
| * | 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 |
| | | | | |||||
| * | | | progress | David Monniaux | 2022-01-24 | 1 | -2/+68 |
| | | | | |||||
| * | | | some progress | David Monniaux | 2022-01-24 | 1 | -1/+25 |
| | | | | |||||
| * | | | fix issue | David Monniaux | 2022-01-24 | 1 | -5/+66 |
| | | | | |||||
| * | | | progress | David Monniaux | 2022-01-24 | 1 | -1/+4 |
| | | | | |||||
| * | | | progress | David Monniaux | 2022-01-24 | 1 | -2/+2 |
| | | | | |||||
| * | | | progress | David Monniaux | 2022-01-24 | 1 | -3/+17 |
| | | | | |||||
| * | | | progress | David Monniaux | 2022-01-24 | 1 | -2/+9 |
| | | | | |||||
| * | | | progress | David Monniaux | 2022-01-24 | 1 | -2/+12 |
| | | | | |||||
| * | | | so that it compiles | David Monniaux | 2022-01-19 | 1 | -2/+58 |
| | | | | |||||
| * | | | find_quotient | David Monniaux | 2022-01-14 | 1 | -0/+64 |
| | | | | |||||
| * | | | find_quotient | David Monniaux | 2022-01-14 | 1 | -7/+17 |
| | | | | |||||
| * | | | some more proof | David Monniaux | 2022-01-14 | 1 | -6/+15 |
| | | | | |||||
| * | | | some progress | David Monniaux | 2022-01-14 | 1 | -0/+75 |
| | | | | |||||
| * | | | relative bound of error | David Monniaux | 2022-01-13 | 1 | -4/+229 |
| | | | | |||||
| * | | | moved functions to a more logical place | David Monniaux | 2022-01-13 | 2 | -191/+180 |
| | | | | |||||
| * | | | more proofs on step1 small b | David Monniaux | 2022-01-12 | 1 | -1/+58 |
| | | | | |||||
| * | | | proof progresses | David Monniaux | 2022-01-12 | 1 | -6/+38 |
| | | | | |||||
| * | | | proof forward | David Monniaux | 2022-01-12 | 1 | -6/+25 |
| | | | | |||||
| * | | | progress in proofs | David Monniaux | 2022-01-12 | 1 | -5/+61 |
| | | | | |||||
| * | | | progress in proofs | David Monniaux | 2022-01-12 | 1 | -224/+30 |
| | | | | |||||
| * | | | proof of approx for a/b | David Monniaux | 2022-01-12 | 1 | -2/+26 |
| | | | | |||||
| * | | | give a name | David Monniaux | 2022-01-12 | 1 | -1/+5 |
| | | | | |||||
| * | | | more proofs | David Monniaux | 2022-01-12 | 1 | -5/+77 |
| | | | | |||||
| * | | | progress in proofs | David Monniaux | 2022-01-12 | 1 | -45/+8 |
| | | | | |||||
 |
index : compcert-kvx | |
| Unnamed repository; edit this file 'description' to name the repository. |
| aboutsummaryrefslogtreecommitdiffstats |