Pierre Roux
Pierre Roux
@ggonthier could you please rebase so that we could merge?
@SnarkBoojum sorry for the late answer, both lemmas indeed look like a worthwhile addition. Would you mind opening a pull request?
@CohenCyril should we postpone this or try to move toward merging?
There seems to be a missing `coq-core` -> `coq-primitive` dependency.
> Why are there both `float64_31` and `float64_63`? Aren't OCaml `float` guaranteed to be 64 bit? Sure, floats are always 64 bits, but on old 32 bits systems, there is...
The fact that some C files are duplicated (but not all) indeed looks really bad. You should probably not copy anything and tell dune to reuse the same C files...
Indeed, my bad. You should probably take the opportunity to move the float int63 conversion functions from uint63_{31,63}.ml to float64_{31,63}.ml, they were put there for historical reasons that no longer...
> For the OCaml library, ocamlfind gives you some leeway, for example `coq.runtime.prim_numbers` could be more descriptive. Maybe `coq.runtime.primitive` or `coq.runtime.primitive_type` since it also contains arrays?
Maybe split into `coq-runtime-number-types` and `coq-runtime-array-type` to avoid persistent arrays to be in something named "number"?
@Lysxia I made the CI a lot "greener" but you still have a few jobs to fix (plugins and test-suite) Note that this definitely conflicts with #15560 so it's probably...