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 /.gitignore | |
| parent | e65eeecf7f34076cbfad6876ec21623ad25e9cf7 (diff) | |
| download | compcert-kvx-647cc8dc9699277cb1e77ae3b07c007186720d59.tar.gz compcert-kvx-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 '.gitignore')
0 files changed, 0 insertions, 0 deletions