diff options
| author | gareuselesinge | 2011-11-08 15:23:52 +0000 |
|---|---|---|
| committer | gareuselesinge | 2011-11-08 15:23:52 +0000 |
| commit | 0cab74bb2906969e5ea72619be3a80dbc48b5675 (patch) | |
| tree | 8810b66531773a4b73654b2e5c2f625988207196 /lib | |
| parent | a0054d400f733bc1761cc1c07ff75b17f94c36f1 (diff) | |
optimization: memoization for is_open_canonical_projection
Assume a pile of constants on the left, and a stuck canonical projection
on the right. We are going to unfold the left constants step by step,
and at every step, we are going to recheck that the very same projection
on the right is stuck. The new check for stuck canonical projections is
more expensive, we thus memoize it for the whole sequence of delta steps
on the left.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14646 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'lib')
0 files changed, 0 insertions, 0 deletions
