Viewing all changes in revision 10121.
- Committer: Maxime Dénès
- Date: 2015-09-09 08:15:48 UTC
- Revision ID: git-v1:3a7cc62147e6b9f9ec9e65fb4387e85b8c4bd03a
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.
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.
- files modified:
- kernel/byterun/coq_interp.c
expand all
collapse all
added
removed
