diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2015-09-06 21:09:48 +0200 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2015-09-06 21:09:48 +0200 |
| commit | 0f8d1b92c37c80e96df2a157a78188d6d94b6e35 (patch) | |
| tree | 373c458574264f9ff9406adc25cf766d3413fdf0 /proofs/tacmach.mli | |
| parent | a5e04d9dd178b2870b79776e1fbf1a858cdac49d (diff) | |
Fix a bug in 31 bit arithmetic, leading to failing conversion tests.
On 64 bits architectures, integers could have some of their 32 msb set to 1
internally in the VM. When read back to a Coq term, this was not observable. But
an equality test would fail. From the user point of view, the symptom was that
vm_compute; reflexivity would succeed but the subsequent Qed would fail.
Bug reported by Tahina Ramananandro.
Diffstat (limited to 'proofs/tacmach.mli')
0 files changed, 0 insertions, 0 deletions