diff options
| author |  msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-01-22 13:13:34 +0000 |
|---|---|---|
| committer | msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-01-22 13:13:34 +0000 |
| commit | e88df65bbc64b18da34a4233f680829025ca76d9 (patch) | |
| tree | f3b0acd95d6b3a45539e755bc7c863e227d97c0a /configure | |
| parent | 9cbec934dfc53c8c2cc589e562331a7a50a8db22 (diff) | |
- Fix evarconv so that we have complete eta-conversion:
- In the maybeflex/rigid (lambda) case, try eta if the maybeflex doesn't
actually unfold (e.g. vars, or the transparent state says it's opaque).
- In the flexible/rigid(lambda) case, try eta if miller-pfenning fails
(as the stack might not be a purely applicative one). This will zip the
flexible term (a case construct most likely) and try eta expansion on it.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16134 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'configure')
0 files changed, 0 insertions, 0 deletions