diff options
author | Xavier Leroy <xavier.leroy@inria.fr> | 2016-12-26 16:55:06 +0100 |
---|---|---|
committer | Xavier Leroy <xavier.leroy@inria.fr> | 2016-12-26 16:55:06 +0100 |
commit | 647cc8dc9699277cb1e77ae3b07c007186720d59 (patch) | |
tree | a37eba4eb015f8b093793858c8f25589fd816af8 /lib/Coqlib.v | |
parent | e65eeecf7f34076cbfad6876ec21623ad25e9cf7 (diff) | |
download | compcert-647cc8dc9699277cb1e77ae3b07c007186720d59.tar.gz compcert-647cc8dc9699277cb1e77ae3b07c007186720d59.zip |
Replace 'decide equality' in x86/Op.v by custom tactics from lib/BoolEqual.v
Applied to the 92-constructor 'operation' type, 'decide equality' produces a huge transparent term that causes the VM compiler to generate huge code and exceeed a memory limit of Coq on 32-bit platforms. (The limit is OCaml's, really.)
The lib/BoolEqual.v file defines alternative tactics to build decidable equalities where the transparent part of the definition is smaller (O(N^2) instead of O(N^3)). The proof parts are still huge (O(N^3)) but they are opaque.
Fixes #151
Diffstat (limited to 'lib/Coqlib.v')
0 files changed, 0 insertions, 0 deletions