Commit message (Collapse) | Author | Age | Files | Lines | |
---|---|---|---|---|---|
* | Replace 'decide equality' in x86/Op.v by custom tactics from lib/BoolEqual.v | Xavier Leroy | 2016-12-26 | 1 | -0/+167 |
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 |