aboutsummaryrefslogtreecommitdiff
path: root/lib
diff options
context:
space:
mode:
authorgareuselesinge2011-11-08 15:23:52 +0000
committergareuselesinge2011-11-08 15:23:52 +0000
commit0cab74bb2906969e5ea72619be3a80dbc48b5675 (patch)
tree8810b66531773a4b73654b2e5c2f625988207196 /lib
parenta0054d400f733bc1761cc1c07ff75b17f94c36f1 (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