diff options
| author | Pierre-Marie Pédrot | 2020-02-02 18:42:25 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-02-02 18:42:25 +0100 |
| commit | 47c1730d4a7c02ba56d0292143f25772319dd98c (patch) | |
| tree | ac5dc6fab5f206e471da5b0f27e4207937561a01 /engine/eConstr.ml | |
| parent | 9c461520c56232e7f7fbebd5134f9e902be1b597 (diff) | |
| parent | e30eab16b2669cfcd63a718fa10a7bc7f6020b8a (diff) | |
Merge PR #11484: Fix 11483 (Performance bug of PrimFLoat.compare with native_compute)
Reviewed-by: maximedenes
Reviewed-by: ppedrot
Diffstat (limited to 'engine/eConstr.ml')
0 files changed, 0 insertions, 0 deletions